Axiom mul0 | index | src |

The base case in the definition of multiplication.

axiom mul0 (a: nat): $ a * 0 = 0 $;