proposition: Lemma CRopp_lt_cancel : forall {R : ConstructiveReals} (r1 r2 : CRcarrier R), - r2 < - r1 -> r1 < r2.
proof: Proof. intros. apply (CRplus_lt_compat_r r1) in H. rewrite (CRplus_opp_l r1) in H. apply (CRplus_lt_compat_l R r2) in H. rewrite CRplus_0_r, (Radd_assoc (CRisRing R)) in H. rewrite CRplus_opp_r, (Radd_0_l (CRisRing R)) in H. exact H. Qed.
imports: QArith Qabs Qround