proposition: Lemma CReal_plus_le_compat_l : forall r r1 r2, r1 <= r2 -> r + r1 <= r + r2.
proof: Proof. intros x y z Hlt contra. apply Hlt. apply CReal_plus_lt_reg_l in contra; exact contra. Qed.
imports: QArith Qpower Qabs Qround Logic.ConstructiveEpsilon Lia Lqa QExtra ConstructiveExtra