Axiom peano1 ≪ | index | src | ≫

axiom peano1 (a: nat): $ suc a != 0 $;