Axiom mulS | index | src |

The successor case in the definition of multiplication.

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