Theorem add02 ≪ | index | src | ≫

theorem add02 (a: nat): $ a + 0 = a $;

Step	Hyp	Ref	Expression
1		add0	a + 0 = a

Axiom use

axs_peano (add0)