Theorem: MyNat.mul_zero (NNG/MyNat/Multiplication.lean)

State before:
a : ℕ
⊢ a * 0 = 0
Tactic:
rfl
State after:
no goals