proposition: Lemma lt_n_nm_m_gt_1 : forall a b : nat, a < a * b -> b > 1.
proof: Proof. intros a b. case b. rewrite <- (mult_n_O a). intro. elim (lt_n_O a). assumption. intro b1. case b1. rewrite <- (mult_n_Sm a 0). rewrite <- (mult_n_O a). simpl in |- *. intro. elim (lt_irrefl a). assumption. intros. apply gt_n_S. apply gt_Sn_O. Qed.
imports: ZArith EqNat