proposition: Lemma natplusassoc (n m k : nat) : ((n + m) + k) = (n + (m + k)).
proof: Proof. revert m k. induction n as [ | n IHn ]. - auto with natarith. - intros. simpl. apply (maponpaths S (IHn m k)). Defined.
imports: UniMath.Foundations.Sets