intro a hi b
case hs

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