Library Coqtail.mytheories.myReals.MyRbasic_fun
Require
Import
Reals
.
Rabs properties
Lemma
Rabs_eq_compat
:
∀
x
y
,
x
=
y
→
Rabs
x
=
Rabs
y
.
Proof
.
intros
x
y
H
;
rewrite
H
;
reflexivity
.
Qed
.