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