proposition: Lemma lt_lt_mult : forall a b c d : nat, a < b -> c < d -> a * c < b * d.
proof: Proof. unfold lt in |- *. intros. apply le_trans with (S a * S c). simpl in |- *. apply le_n_S. rewrite <- (mult_n_Sm a c). rewrite (plus_comm c (a * c + a)). apply le_plus_trans. apply le_plus_trans. apply le_n. apply le_le_mult. assumption. assumption. Qed.
imports: ZArith EqNat