Theorem mul02 ≪ | index | src | ≫

theorem mul02 (a: nat): $ a * 0 = 0 $;

Step	Hyp	Ref	Expression
1		mul0	a * 0 = 0

Axiom use

axs_peano (mul0)