no goals
n m k : Nat
⊢ (n - m) * k = n * k - m * k
induction m with
| zero => simp
| succ m ih => rw [Nat.sub_succ, Nat.mul_pred_left, ih, succ_mul, Nat.sub_sub]; done
no goals
case zero
n k : Nat
⊢ (n - zero) * k = n * k - zero * k
simp
no goals
case succ
n k m : Nat
ih : (n - m) * k = n * k - m * k
⊢ (n - succ m) * k = n * k - succ m * k
rw [Nat.sub_succ, Nat.mul_pred_left, ih, succ_mul, Nat.sub_sub]