Library Coqtail.mytheories.myReals.MyRbasic_fun


Require Import Reals.

Rabs properties


Lemma Rabs_eq_compat : x y, x = yRabs x = Rabs y.
Proof.
 intros x y H; rewrite H; reflexivity.
Qed.