Axiom peano2 | index | src |

The successor function is injective. Axiom 2 of Peano Arithmetic.

axiom peano2 (a b: nat): $ suc a = suc b <-> a = b $;