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