no goals
n m : Nat
⊢ pred n * m = n * m - m
cases n with
| zero   => simp
| succ n => rw [Nat.pred_succ, succ_mul, Nat.add_sub_cancel]
no goals
case zero
m : Nat
⊢ pred zero * m = zero * m - m
simp
no goals
case succ
m n : Nat
⊢ pred (succ n) * m = succ n * m - m
rw [Nat.pred_succ, succ_mul, Nat.add_sub_cancel]