Axiom addS | index | src |

The successor case in the definition of addition.

axiom addS (a b: nat): $ a + suc b = suc (a + b) $;