Lemma natmultassoc (n m k : nat) : ((n * m) * k) = (n * (m * k)). Proof. induction n as [ | n IHn ]. - apply idpath. - simpl. rewrite natrdistr. apply (maponpaths (λ x, x + m * k)). apply IHn. Defined.