a b : Nat
⊢ a * b + b + succ a = a * b + b + a + 1
a b : Nat
⊢ succ a * succ b = a * b + a + b + 1
rw [mul_succ, succ_mul, Nat.add_right_comm _ a]
no goals
a b : Nat
⊢ a * b + b + succ a = a * b + b + a + 1
rfl