Theorem addS2 ≪ | index | src | ≫

theorem addS2 (a b: nat): $ a + suc b = suc (a + b) $;

Step	Hyp	Ref	Expression
1		addS	a + suc b = suc (a + b)

Axiom use

axs_peano (addS)