Axiom
mul0
≪
|
index
|
src
|
≫
The base case in the definition of multiplication.
axiom mul0 (a: nat): $ a * 0 = 0 $;