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