Lemma multnsm (n m : nat) : n * S m = n + n * m. Proof. revert m. induction n as [|n IHn]. - intros. apply idpath. - intro m. simpl. rewrite <- natplusassoc. rewrite (natpluscomm _ m). change (S (m + (n + n * m))) with (S m + (n + n * m)). rewrite (natpluscomm (S m) _). apply (maponpaths (λ x, x + S m)). apply IHn. Defined.