proposition: Lemma CRabs_def1 : forall {R : ConstructiveReals} (x y : CRcarrier R), x < y -> -x < y -> CRabs _ x < y.
proof: Proof. intros. destruct (CRltLinear R), p. destruct (s x (CRabs R x) y H). 2: exact c0. rewrite CRabs_left. - exact H0. - intro abs. rewrite CRabs_right in c0. + exact (CRlt_asym x x c0 c0). + apply CRlt_asym, abs. Qed.
imports: QArith Qabs ConstructiveReals