-ntheorem psym_plus: ∀n,m. n + m = m + n.
- #n; nelim n
- [ #m; nelim m; //; #n0; #H;
- nchange with (natS n0 = natS (n0 + O));
- nrewrite < H; //
- | #n0; #H; #m; nchange with (S (n0 + m) = m + S n0);
- nrewrite > (H …);
- nelim m; //;
- #n1; #E; nrewrite > E; //]