Lemma natmultcomm (n m : nat) : (n * m) = (m * n). Proof. revert m. induction n as [ | n IHn ]. - intro. auto with natarith. - intro m. rewrite (multsnm n m). rewrite (multnsm m n). apply (maponpaths (λ x : _, m + x) (IHn m)). Defined.