proposition: Lemma CReal_plus_le_reg_r : forall x y z : CReal, y + x <= z + x -> y <= z.
proof: Proof. intros x y z Hlt contra. apply Hlt. apply CReal_plus_lt_compat_r; exact contra. Qed.
imports: QArith Qpower Qabs Qround Logic.ConstructiveEpsilon Lia Lqa QExtra ConstructiveExtra