exact
  calc
    succ a * succ b' = succ a * (b' + one) := by rw [succ_eq_add_one b']
    _                = succ a * b' + succ a * one := by rw [mul_add]
    _                = succ a * b' + succ a := by rw [mul_one]
    _                = a * b' + b' + succ a := by rw [ih]
    _                = a * b' + succ a + b' := by rw [add_comm_right]
    _                = a * b' + (a + one) + b' := by rw [succ_eq_add_one]
    _                = a * b' + a + one + b' := by simp only [add_assoc]
    _                = a * succ b' + one + b' := by rw [← mul_succ]
    _                = a * succ b' + b' + one := by rw [add_comm_right]
    _                = a * succ b' + (b' + one) := by rw [add_assoc]
    _                = a * succ b' + succ b' := by rw [succ_eq_add_one]
case succ
a b' : Nat
ih : succ a * b' = a * b' + b'
⊢ succ a * succ b' = a * succ b' + succ b'
no goals