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