proposition: Lemma CRabs_lt : forall {R : ConstructiveReals} (x y : CRcarrier R), CRabs _ x < y -> prod (x < y) (-x < y).
proof: Proof. split. - apply (CRle_lt_trans _ _ _ (CRle_abs x)), H. - apply (CRle_lt_trans _ _ _ (CRle_abs (-x))). rewrite CRabs_opp. exact H. Qed.
imports: QArith Qabs ConstructiveReals