proposition: Lemma Zlt_mult_mult : forall a b c d : Z, (0 < a)%Z -> (0 < d)%Z -> (a < b)%Z -> (c < d)%Z -> (a * c < b * d)%Z.
proof: Proof. intros. apply Z.lt_trans with (a * d)%Z. apply Zlt_reg_mult_l. Flip. assumption. rewrite Zmult_comm. rewrite Zmult_comm with b d. apply Zlt_reg_mult_l. Flip. assumption. Qed.
imports: Coq(Lia)