intro c hi a b
case hs

⊢ ∀ (n : ↑N0),
    (∀ (a b : ↑N0), mul (mul (a, b), n) = mul (a, mul (b, n))) →
      ∀ (a b : ↑N0), mul (mul (a, b), S n) = mul (a, mul (b, S n))
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))