proposition: Lemma lt_n_nm : forall n m : nat, 0 < n -> 1 < m -> n < n * m.
proof: Proof. intros n m. case n. intros. elim (lt_n_O 0). assumption. intro n1. case m. intros. elim (lt_n_O 1). assumption. intro m1. case m1. intros. elim (lt_irrefl 1). assumption. intro m2. elim n1. simpl in |- *. intros. apply lt_n_S. apply lt_O_Sn. simpl in |- *. intros n2 IH. intros. apply lt_n_S. apply lt_trans with (S (S (m2 + n2 * S (S m2)))). apply IH. apply lt_O_Sn. apply lt_n_S. apply lt_O_Sn. apply lt_n_S. rewrite (plus_comm m2). rewrite (plus_comm m2). simpl in |- *. apply lt_n_S. apply lt_le_trans with (S (n2 * S (S m2) + m2)). apply lt_n_Sn. apply le_n_S. apply le_plus_trans. apply le_n. Qed.
imports: ZArith EqNat