proposition: Lemma CReal_plus_lt_reg_l : forall x y z : CReal, x + y < x + z -> y < z.
proof: Proof. intros x y z Hlt. destruct Hlt as [n maj]; exists (n - 1)%Z. setoid_replace (seq z (n - 1)%Z - seq y (n - 1)%Z)%Q with (seq (CReal_plus x z) n - seq (CReal_plus x y) n)%Q. - rewrite Qpower_minus_pos. assert (2 ^ n > 0)%Q by (apply Qpower_0_lt; lra); lra. - unfold CReal_plus, CReal_plus_seq in maj |- *. do 2 rewrite CReal_red_seq in maj |- *. do 2 rewrite Qred_correct; ring. Qed.
imports: QArith Qpower Qabs Qround Logic.ConstructiveEpsilon Lia Lqa QExtra ConstructiveExtra