specialize hi a b
case hs
c : ↑N0
hi : ∀ (a b : ↑N0), mul (mul (a, b), c) = mul (a, mul (b, c))
a b : ↑N0
⊢ mul (mul (a, b), S c) = mul (a, mul (b, S c))
case hs
c a b : ↑N0
hi : mul (mul (a, b), c) = mul (a, mul (b, c))
⊢ mul (mul (a, b), S c) = mul (a, mul (b, S c))