proposition: Lemma le_n_nm : forall n m : nat, n <= n * S m.
proof: Proof. simple induction n. simpl in |- *. intros. apply le_n. intros n1 IHn1. simpl in |- *. intros. apply le_n_S. rewrite (plus_comm m (n1 * S m)). apply le_plus_trans. apply IHn1. Qed.
imports: ZArith EqNat