in citp
in pnat

fmod PNAT-L is
 inc PNAT .
 vars M N : PNat .
 eq N + 0 = N          [metadata "lemma-1"].
 eq M + s N = s(M + N) [metadata "lemma-2"]. 
endfm

select #CITP# .
loop init .

---> Proof of commutativity:
*** 1 ***
(goal PNAT-L |-
eq M:PNat + N:PNat = N:PNat + M:PNat ;)
*** 2 ***
(ind on M:PNat)
*** 3 ***
(tc red)
---> QED