proposition: Lemma CRplus_le_reg_r : forall {R : ConstructiveReals} (r r1 r2 : CRcarrier R), r1 + r <= r2 + r -> r1 <= r2.
proof: Proof. intros. intro abs. apply H. clear H. apply CRplus_lt_compat_r. exact abs. Qed.
imports: QArith Qabs Qround