no goals
n m : Nat
⊢ succ n * m = n * m + m
induction m with
| zero => rfl
| succ m ih => rw [mul_succ, add_succ, ih, mul_succ, add_succ, Nat.add_right_comm]
no goals
case zero
n : Nat
⊢ succ n * zero = n * zero + zero
rfl
no goals
case succ
n m : Nat
ih : succ n * m = n * m + m
⊢ succ n * succ m = n * succ m + succ m
rw [mul_succ, add_succ, ih, mul_succ, add_succ, Nat.add_right_comm]