proposition: Lemma CReal_plus_lt_compat_r : forall x y z : CReal, y < z -> y + x < z + x.
proof: Proof. intros x y z. do 2 rewrite <- (CReal_plus_comm x). apply CReal_plus_lt_compat_l. Qed.
imports: QArith Qpower Qabs Qround Logic.ConstructiveEpsilon Lia Lqa QExtra ConstructiveExtra