proposition: Lemma gt_1_mult_lt_compat_r x y z : 1 < z -> 0 < y -> x < y -> x < y * z.
proof: Proof. intros. transitivity y; [ trivial |]. pattern y at 1;apply (transport _ (mult_1_r y)). apply (strictly_order_preserving_pos (.*.) y);trivial. Qed.
imports: HoTT.Classes.theory.apartness HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.interfaces.orders HoTT.Classes.theory.rings HoTT.Classes.orders.orders HoTT.Classes.orders.maps