proposition: Lemma CReal_plus_lt_reg_r : forall x y z : CReal, y + x < z + x -> y < z.
proof: Proof. intros x y z Hlt. rewrite (CReal_plus_comm y), (CReal_plus_comm z) in Hlt. apply CReal_plus_lt_reg_l in Hlt; exact Hlt. Qed.
imports: QArith Qpower Qabs Qround Logic.ConstructiveEpsilon Lia Lqa QExtra ConstructiveExtra