proposition: Lemma Zmult_lt_compat2 n m p q : 0 < n <= p -> 0 < m < q -> n * m < p * q.
proof: Proof. intros (Hn, Hnp) (Hm,Hmq). apply Z.le_lt_trans with (p * m). - apply Z.mul_le_mono_pos_r; trivial. - apply Z.mul_lt_mono_pos_l; Z.order. Qed.
imports: BinPos BinInt Decidable Zcompare Arith_base