proposition: Lemma CRabs_pos : forall {R : ConstructiveReals} (x : CRcarrier R), 0 <= CRabs R x.
proof: Proof. intros. intro abs. destruct (CRltLinear R). clear p. specialize (s _ x _ abs). destruct s. - exact (CRle_abs x c). - rewrite CRabs_left in abs. + rewrite <- CRopp_0 in abs. apply CRopp_lt_cancel in abs. exact (CRlt_asym _ _ abs c). + apply CRlt_asym, c. Qed.
imports: QArith Qabs ConstructiveReals