forall a b c d, 0 <= a /\ a <= b -> 0 < b -> 0 <= c /\ c < d -> a * c < b * d. Proof. intros a b c d [E1 E2] E3 [E4 E5] . apply le_lt_trans with (b * c). - apply mult_le_compat;auto. - apply (strictly_order_preserving (b *.)). trivial. Qed.
Require Import