Theorem: Nat.mod2_succ_eq_one (Lib.lean)

State before:
n : ℕ
⊢ (n + 1) % 2 = 1 ↔ n % 2 = 0
Tactic:
cases n using binaryRec with
| z => simp
| f b _ _ => cases b <;> simp [← Nat.two_mul, Nat.mul_add_mod]
State after:
no goals

State before:
case z

⊢ (0 + 1) % 2 = 1 ↔ 0 % 2 = 0
Tactic:
simp
State after:
no goals

State before:
case f
b : Bool
n✝ : ℕ
a✝ : bit b n✝ = n✝ → ((bit b n✝ + 1) % 2 = 1 ↔ bit b n✝ % 2 = 0)
⊢ (bit b n✝ + 1) % 2 = 1 ↔ bit b n✝ % 2 = 0
Tactic:
cases b <;> simp [← Nat.two_mul, Nat.mul_add_mod]
State after:
no goals