x y z : 1 < z -> 0 < y -> x < y -> x < y * z. Proof. intros. transitivity y; [ trivial |]. pattern y at 1;apply (transport _ (mult_1_r y)). apply (strictly_order_preserving_pos (.*.) y);trivial. Qed.
Require Import