apply generic_recursor
⊢ ∀ (b a : ↑N0), mul (S a, b) = plus (mul (a, b), b)
case hz

⊢ ∀ (a : ↑N0), mul (S a, z) = plus (mul (a, z), z)

case hs

⊢ ∀ (n : ↑N0),
    (∀ (a : ↑N0), mul (S a, n) = plus (mul (a, n), n)) → ∀ (a : ↑N0), mul (S a, S n) = plus (mul (a, S n), S n)