Theorem: Nat.div_mod2 (Lib.lean)

State before:
n : ℕ
⊢ n / 2 + n % 2 = (n + 1) / 2
Tactic:
induction n using Nat.binaryRec' with
| z => rfl
| f b _ _ _ => cases b <;> simp [bit_val, mul_add_div, mul_add_mod]
State after:
no goals

State before:
case z

⊢ 0 / 2 + 0 % 2 = (0 + 1) / 2
Tactic:
rfl
State after:
no goals

State before:
case f
b : Bool
n✝ : ℕ
a✝¹ : n✝ = 0 → b = true
a✝ : n✝ / 2 + n✝ % 2 = (n✝ + 1) / 2
⊢ bit b n✝ / 2 + bit b n✝ % 2 = (bit b n✝ + 1) / 2
Tactic:
cases b <;> simp [bit_val, mul_add_div, mul_add_mod]
State after:
no goals