proposition: Lemma CReal_plus_lt_compat_l : forall x y z : CReal, y < z -> x + y < x + z.
proof: Proof. intros x y z Hlt. apply CRealLt_above in Hlt; destruct Hlt as [n Hapart]; exists n. unfold CReal_plus, CReal_plus_seq in Hapart |- *. do 2 rewrite CReal_red_seq. do 2 rewrite Qred_correct. specialize (Hapart (n-1)%Z ltac:(lia)). lra. Qed.
imports: QArith Qpower Qabs Qround Logic.ConstructiveEpsilon Lia Lqa QExtra ConstructiveExtra