proposition: Lemma CRabs_minus_sym : forall {R : ConstructiveReals} (x y : CRcarrier R), CRabs R (x - y) == CRabs R (y - x).
proof: Proof. intros R x y. setoid_replace (x - y) with (-(y-x)). - rewrite CRabs_opp. reflexivity. - unfold CRminus. rewrite CRopp_plus_distr, CRplus_comm, CRopp_involutive. reflexivity. Qed.
imports: QArith Qabs ConstructiveReals