Lemma natldistr (m k n : nat) : (n * (m + k)) = (n * m + n * k). Proof. induction m as [ | m IHm ]. - simpl. rewrite (natmultn0 n). auto with natarith. - simpl. rewrite (multnsm n (m + k)). rewrite (multnsm n m). rewrite (natplusassoc _ _ _). apply (maponpaths (λ x : _, n + x) (IHm)). Defined.