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