Theorem mulS2 ≪ | index | src | ≫

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

Step	Hyp	Ref	Expression
1		mulS	a * suc b = a * b + a

Axiom use

axs_peano (mulS)