The successor function is injective. Axiom 2 of Peano Arithmetic.
axiom peano2 (a b: nat): $ suc a = suc b <-> a = b $;