proposition: Lemma CRplus_appart_reg_l : forall {R : ConstructiveReals} (r r1 r2 : CRcarrier R), (r + r1) ≶ (r + r2) -> r1 ≶ r2.
proof: Proof. intros. destruct H. - left. apply (CRplus_lt_reg_l R r), c. - right. apply (CRplus_lt_reg_l R r), c. Qed.
imports: QArith Qabs Qround