proposition: Lemma mult_lt_compat x₁ y₁ x₂ y₂ : 0 < x₁ → 0 < x₂ → x₁ < y₁ → x₂ < y₂ → x₁ * x₂ < y₁ * y₂.
proof: Proof. intros Ex₁ Ey₁ E1 E2. transitivity (y₁ * x₂). now apply (strictly_order_preserving_flip_pos (.*.) x₂). apply (strictly_order_preserving_pos (.*.) y₁); [| easy ]. now transitivity x₁. Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.theory.rings MathClasses.orders.orders MathClasses.orders.maps