x₁ y₁ x₂ y₂ : x₁ ≤ y₁ -> x₂ < y₂ -> x₁ + x₂ < y₁ + y₂. Proof. intros E1 E2. apply le_lt_trans with (y₁ + x₂). - apply (order_preserving (+ x₂));trivial. - apply (strictly_order_preserving (y₁ +));trivial. Qed.
Require Import