proposition: Lemma mult_n_Sm : forall n m:nat, n * m + n = n * S m.
proof: Proof. intros n m; induction n as [| p H]; simpl; auto. destruct H; rewrite <- plus_n_Sm; apply eq_S. pattern m at 1 3; elim m; simpl; auto. Qed.
imports: Notations Ltac Datatypes Logic