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