The successor case in the definition of addition.
axiom addS (a b: nat): $ a + suc b = suc (a + b) $;