Theorem b1ne0 ≪ | index | src | ≫

theorem b1ne0 (n: nat): $ b1 n != 0 $;

Step	Hyp	Ref	Expression
1		peano1	suc (b0 n) != 0
2	1	conv b1	b1 n != 0

Axiom use

axs_peano (peano1)