proposition: Lemma CReal_plus_le_lt_compat : forall r1 r2 r3 r4 : CReal, r1 <= r2 -> r3 < r4 -> r1 + r3 < r2 + r4.
proof: Proof. intros r1 r2 r3 r4 Hr1ler2 Hr3ltr4. apply CReal_le_lt_trans with (r2 + r3). - intro contra; rewrite CReal_plus_comm, (CReal_plus_comm r1) in contra. apply CReal_plus_lt_reg_l in contra. contradiction. - apply CReal_plus_lt_compat_l. exact Hr3ltr4. Qed.
imports: QArith Qpower Qabs Qround Logic.ConstructiveEpsilon Lia Lqa QExtra ConstructiveExtra