Lemma natpluscomm (n m : nat) : n + m = m + n. Proof. revert m. induction n as [ | n IHn ]. - intro. auto with natarith. - intro. set (int := IHn (S m)). set (int2 := pathsinv0 (natplusnsm n m)). set (int3 := pathsinv0 (natplusnsm m n)). set (int4 := pathscomp0 int2 int). apply (pathscomp0 int4 int3). Defined.