Theorem: Poland1998P4.lemma2 (Compfiles/Poland1998P4.lean)

State before:
n : ℕ
⊢ (2 * n + 1) / 2 = n
Tactic:
rw [Nat.mul_add_div (Nat.le.step Nat.le.refl) n 1]
State after:
n : ℕ
⊢ n + 1 / (Nat.succ 0).succ = n

State before:
n : ℕ
⊢ n + 1 / (Nat.succ 0).succ = n
Tactic:
simp only [Nat.reduceSucc, Nat.reduceDiv, add_zero]
State after:
no goals