proposition: Lemma pos_mult_le_lt_compat : forall a b c d, 0 <= a /\ a <= b -> 0 < b -> 0 <= c /\ c < d -> a * c < b * d.
proof: 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.
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