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