diff --git a/src/Init/Core.lean b/src/Init/Core.lean
index 3b921fc12631..80e5b84699f1 100644
--- a/src/Init/Core.lean
+++ b/src/Init/Core.lean
@@ -680,6 +680,11 @@ theorem Eq.substr {α : Sort u} {p : α → Prop} {a b : α} (h₁ : b = a) (h
 theorem cast_eq {α : Sort u} (h : α = α) (a : α) : cast h a = a :=
   rfl
 
+theorem eqRec_eq_cast {α : Sort _} {a : α} {motive : (a' : α) → a = a' → Sort _}
+    (x : motive a (rfl : a = a)) {a' : α} (e : a = a') :
+    @Eq.rec α a motive x a' e = cast (e ▸ rfl) x := by
+  subst e; rfl
+
 /--
 `a ≠ b`, or `Ne a b` is defined as `¬ (a = b)` or `a = b → False`,
 and asserts that `a` and `b` are not equal.
diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index deee66a75187..0d003ab01794 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -137,8 +137,7 @@ theorem msb_eq_getLsb_last (x : BitVec w) :
     x.getLsb (w-1) = decide (2 ^ (w-1) ≤ x.toNat) := by
   rcases w with rfl | w
   · simp
-  · simp only [Nat.zero_lt_succ, decide_True, getLsb, Nat.testBit, Nat.succ_sub_succ_eq_sub,
-    Nat.sub_zero, Nat.and_one_is_mod, Bool.true_and, Nat.shiftRight_eq_div_pow]
+  · simp only [getLsb, Nat.testBit_to_div_mod, Nat.succ_sub_succ_eq_sub, Nat.sub_zero]
     rcases (Nat.lt_or_ge (BitVec.toNat x) (2 ^ w)) with h | h
     · simp [Nat.div_eq_of_lt h, h]
     · simp only [h]
@@ -506,7 +505,6 @@ theorem getMsb_rev (x : BitVec w) (i : Fin w) :
     have p2 : i ≠ n := by omega
     simp [p1, p2]
   · simp [i_eq_n, testBit_toNat]
-    cases b <;> trivial
   · have p1 : i ≠ n := by omega
     have p2 : i - n ≠ 0 := by omega
     simp [p1, p2, Nat.testBit_bool_to_nat]
diff --git a/src/Init/Data/Bool.lean b/src/Init/Data/Bool.lean
index be1e924300cd..63893b7c121f 100644
--- a/src/Init/Data/Bool.lean
+++ b/src/Init/Data/Bool.lean
@@ -210,9 +210,6 @@ theorem and_or_inj_left_iff :
 
 /-! ## toNat -/
 
-/-- convert a `Bool` to a `Nat`, `false -> 0`, `true -> 1` -/
-def toNat (b:Bool) : Nat := cond b 1 0
-
 @[simp] theorem toNat_false : false.toNat = 0 := rfl
 
 @[simp] theorem toNat_true : true.toNat = 1 := rfl
@@ -229,6 +226,8 @@ theorem toNat_lt (b : Bool) : b.toNat < 2 :=
   cases b <;> simp
 @[simp] theorem toNat_eq_one (b : Bool) : b.toNat = 1 ↔ b = true := by
   cases b <;> simp
+@[simp] theorem toNat_mod_two (b : Bool) : b.toNat % 2 = b.toNat := by
+  cases b <;> simp
 
 end Bool
 
diff --git a/src/Init/Data/Nat/Bitwise/Basic.lean b/src/Init/Data/Nat/Bitwise/Basic.lean
index 57e6bb3515df..cf85170834c7 100644
--- a/src/Init/Data/Nat/Bitwise/Basic.lean
+++ b/src/Init/Data/Nat/Bitwise/Basic.lean
@@ -8,6 +8,9 @@ import Init.Data.Nat.Basic
 import Init.Data.Nat.Div
 import Init.Coe
 
+/-- convert a `Bool` to a `Nat`, `false => 0`, `true => 1` -/
+def Bool.toNat (b : Bool) : Nat := cond b 1 0
+
 namespace Nat
 
 theorem bitwise_rec_lemma {n : Nat} (hNe : n ≠ 0) : n / 2 < n :=
@@ -51,6 +54,31 @@ instance : Xor Nat := ⟨Nat.xor⟩
 instance : ShiftLeft Nat := ⟨Nat.shiftLeft⟩
 instance : ShiftRight Nat := ⟨Nat.shiftRight⟩
 
+theorem shiftLeft_eq (a b : Nat) : a <<< b = a * 2 ^ b :=
+  match b with
+  | 0 => (Nat.mul_one _).symm
+  | b+1 => (shiftLeft_eq _ b).trans <| by
+    simp [Nat.pow_succ, Nat.mul_assoc, Nat.mul_left_comm, Nat.mul_comm]
+
+@[simp] theorem shiftRight_zero : n >>> 0 = n := rfl
+
+theorem shiftRight_succ (m n) : m >>> (n + 1) = (m >>> n) / 2 := rfl
+
+theorem shiftRight_add (m n : Nat) : ∀ k, m >>> (n + k) = (m >>> n) >>> k
+  | 0 => rfl
+  | k + 1 => by simp [← Nat.add_assoc, shiftRight_add _ _ k, shiftRight_succ]
+
+theorem shiftRight_eq_div_pow (m : Nat) : ∀ n, m >>> n = m / 2 ^ n
+  | 0 => (Nat.div_one _).symm
+  | k + 1 => by
+    rw [shiftRight_add, shiftRight_eq_div_pow m k]
+    simp [Nat.div_div_eq_div_mul, ← Nat.pow_succ, shiftRight_succ]
+
+/-- `bit b` appends the digit `b` to the little end of the binary representation of
+  its natural number input. -/
+def bit (b : Bool) (n : Nat) : Nat :=
+  cond b (n + n + 1) (n + n)
+
 /-!
 ### testBit
 We define an operation for testing individual bits in the binary representation
@@ -58,6 +86,82 @@ of a number.
 -/
 
 /-- `testBit m n` returns whether the `(n+1)` least significant bit is `1` or `0`-/
-def testBit (m n : Nat) : Bool := (m >>> n) &&& 1 != 0
+def testBit (m n : Nat) : Bool := 1 &&& (m >>> n) != 0
+-- `1 &&& n` is faster than `n &&& 1` for big `n`. This may change in the future.
+
+theorem bit_val (b n) : bit b n = 2 * n + b.toNat := by
+  rw [Nat.mul_comm]
+  induction b with
+  | false => exact congrArg (· + n) n.zero_add.symm
+  | true => exact congrArg (· + n + 1) n.zero_add.symm
+
+theorem shiftRight_one (n) : n >>> 1 = n / 2 := rfl
+
+theorem mod_two_eq_zero_or_one (n : Nat) : n % 2 = 0 ∨ n % 2 = 1 :=
+  match n % 2, @Nat.mod_lt n 2 (by decide) with
+  | 0, _ => .inl rfl
+  | 1, _ => .inr rfl
+
+@[simp] theorem one_land_eq_mod_two (n : Nat) : 1 &&& n = n % 2 := by
+  match Nat.decEq n 0 with
+  | isTrue n0 => subst n0; decide
+  | isFalse n0 =>
+    simp only [HAnd.hAnd, AndOp.and, land]
+    unfold bitwise
+    cases mod_two_eq_zero_or_one n with | _ h => simp [n0, h]; rfl
+
+@[simp]
+theorem testBit_zero (n : Nat) : testBit n 0 = decide (n % 2 = 1) := by
+  cases mod_two_eq_zero_or_one n with | _ h => simp [testBit, h]
+
+@[simp] theorem decide_mod_two_eq_one_toNat (n : Nat) : (decide (n % 2 = 1)).toNat = n % 2 := by
+  cases mod_two_eq_zero_or_one n with | _ h => simp [h]; rfl
+
+theorem testBit_zero_toNat (n : Nat) : (n.testBit 0).toNat = n % 2 := by simp
+
+theorem bit_decomp (n : Nat) : bit (n.testBit 0) (n >>> 1) = n := by
+  simp [bit_val, shiftRight_one, Nat.div_add_mod]
+
+theorem bit_eq_zero_iff {n : Nat} {b : Bool} : bit b n = 0 ↔ n = 0 ∧ b = false := by
+  cases n <;> cases b <;> simp [bit, ← Nat.add_assoc]
+
+/-- For a predicate `C : Nat → Sort u`, if instances can be
+  constructed for natural numbers of the form `bit b n`,
+  they can be constructed for any given natural number. -/
+@[inline]
+def bitCasesOn {C : Nat → Sort u} (n) (h : ∀ b n, C (bit b n)) : C n := bit_decomp n ▸ h _ _
+
+/-- A recursion principle for `bit` representations of natural numbers.
+  For a predicate `C : Nat → Sort u`, if instances can be
+  constructed for natural numbers of the form `bit b n`,
+  they can be constructed for all natural numbers. -/
+@[elab_as_elim, specialize]
+def binaryRec {C : Nat → Sort u} (z : C 0) (f : ∀ b n, C n → C (bit b n)) (n : Nat) : C n :=
+  if n0 : n = 0 then congrArg C n0 ▸ z -- `congrArg C _` is `rfl` in non-dependent case
+  else congrArg C n.bit_decomp ▸ f (1 &&& n != 0) (n >>> 1) (binaryRec z f (n >>> 1))
+decreasing_by exact bitwise_rec_lemma n0
+
+/-- The same as `binaryRec`, but the induction step can assume that if `n=0`,
+  the bit being appended is `true`-/
+@[elab_as_elim, specialize]
+def binaryRec' {C : Nat → Sort u} (z : C 0)
+    (f : ∀ b n, (n = 0 → b = true) → C n → C (bit b n)) : ∀ n, C n :=
+  binaryRec z fun b n ih =>
+    if h : n = 0 → b = true then f b n h ih
+    else
+      have : bit b n = 0 := by
+        rw [bit_eq_zero_iff]
+        cases n <;> cases b <;> simp at h <;> simp [h]
+      congrArg C this ▸ z
+
+/-- The same as `binaryRec`, but special casing both 0 and 1 as base cases -/
+@[elab_as_elim, specialize]
+def binaryRecFromOne {C : Nat → Sort u} (z₀ : C 0) (z₁ : C 1)
+    (f : ∀ b n, n ≠ 0 → C n → C (bit b n)) : ∀ n, C n :=
+  binaryRec' z₀ fun b n h ih =>
+    if h' : n = 0 then by
+      rw [h', h h']
+      exact z₁
+    else f b n h' ih
 
 end Nat
diff --git a/src/Init/Data/Nat/Bitwise/Lemmas.lean b/src/Init/Data/Nat/Bitwise/Lemmas.lean
index 2085a2fec004..cbc4cfe7b0fb 100644
--- a/src/Init/Data/Nat/Bitwise/Lemmas.lean
+++ b/src/Init/Data/Nat/Bitwise/Lemmas.lean
@@ -33,21 +33,6 @@ private theorem two_mul_sub_one {n : Nat} (n_pos : n > 0) : (2*n - 1) % 2 = 1 :=
 
 /-! ### Preliminaries -/
 
-/--
-An induction principal that works on divison by two.
--/
-noncomputable def div2Induction {motive : Nat → Sort u}
-    (n : Nat) (ind : ∀(n : Nat), (n > 0 → motive (n/2)) → motive n) : motive n := by
-  induction n using Nat.strongInductionOn with
-  | ind n hyp =>
-    apply ind
-    intro n_pos
-    if n_eq : n = 0 then
-      simp [n_eq] at n_pos
-    else
-      apply hyp
-      exact Nat.div_lt_self n_pos (Nat.le_refl _)
-
 @[simp] theorem zero_and (x : Nat) : 0 &&& x = 0 := by rfl
 
 @[simp] theorem and_zero (x : Nat) : x &&& 0 = 0 := by
@@ -55,29 +40,48 @@ noncomputable def div2Induction {motive : Nat → Sort u}
   unfold bitwise
   simp
 
-@[simp] theorem and_one_is_mod (x : Nat) : x &&& 1 = x % 2 := by
-  if xz : x = 0 then
-    simp [xz, zero_and]
-  else
-    have andz := and_zero (x/2)
-    simp only [HAnd.hAnd, AndOp.and, land] at andz
-    simp only [HAnd.hAnd, AndOp.and, land]
-    unfold bitwise
-    cases mod_two_eq_zero_or_one x with | _ p =>
-      simp [xz, p, andz, one_div_two, mod_eq_of_lt]
+/-! ### bitwise -/
+
+@[simp]
+theorem bitwise_zero_left (m : Nat) : bitwise f 0 m = if f false true then m else 0 :=
+  rfl
+
+@[simp]
+theorem bitwise_zero_right (n : Nat) : bitwise f n 0 = if f true false then n else 0 := by
+  unfold bitwise
+  simp only [ite_self, decide_False, Nat.zero_div, ite_true]
+  cases n <;> simp
+
+theorem bitwise_zero : bitwise f 0 0 = 0 := by
+  simp only [bitwise_zero_right, ite_self]
+
+/-! ### bit -/
+
+@[simp]
+theorem bit_div_two (b n) : bit b n / 2 = n := by
+  rw [bit_val, Nat.add_comm, add_mul_div_left, div_eq_of_lt, Nat.zero_add]
+  · cases b <;> decide
+  · decide
+
+@[simp]
+theorem bit_mod_two (b n) : bit b n % 2 = b.toNat := by
+  cases b <;> simp [bit_val, mul_add_mod]
+
+theorem mul_two_le_bit {x b n} : x * 2 ≤ bit b n ↔ x ≤ n := by
+  rw [← le_div_iff_mul_le Nat.two_pos, bit_div_two]
 
 /-! ### testBit -/
 
 @[simp] theorem zero_testBit (i : Nat) : testBit 0 i = false := by
-  simp only [testBit, zero_shiftRight, zero_and, bne_self_eq_false]
-
-@[simp] theorem testBit_zero (x : Nat) : testBit x 0 = decide (x % 2 = 1) := by
-  cases mod_two_eq_zero_or_one x with | _ p => simp [testBit, p]
+  simp only [testBit, zero_shiftRight, and_zero, bne_self_eq_false]
 
-@[simp] theorem testBit_succ (x i : Nat) : testBit x (succ i) = testBit (x/2) i := by
+@[simp] theorem testBit_succ (x i : Nat) : testBit x (i + 1) = testBit (x / 2) i := by
   unfold testBit
   simp [shiftRight_succ_inside]
 
+theorem bit_testBit_zero (b n) : (bit b n).testBit 0 = b := by
+  simp
+
 theorem testBit_to_div_mod {x : Nat} : testBit x i = decide (x / 2^i % 2 = 1) := by
   induction i generalizing x with
   | zero =>
@@ -86,46 +90,37 @@ theorem testBit_to_div_mod {x : Nat} : testBit x i = decide (x / 2^i % 2 = 1) :=
   | succ i hyp =>
     simp [hyp, Nat.div_div_eq_div_mul, Nat.pow_succ']
 
+@[simp] theorem _root_.Bool.toNat_testBit_zero (b : Bool) : b.toNat.testBit 0 = b := by
+  cases b <;> rfl
+
+theorem toNat_testBit (x i : Nat) :
+    (x.testBit i).toNat = x / 2 ^ i % 2 := by
+  rw [Nat.testBit_to_div_mod]
+  rcases Nat.mod_two_eq_zero_or_one (x / 2^i) <;> simp_all
+
 theorem ne_zero_implies_bit_true {x : Nat} (xnz : x ≠ 0) : ∃ i, testBit x i := by
-  induction x using div2Induction with
-  | ind x hyp =>
-    have x_pos : x > 0 := Nat.pos_of_ne_zero xnz
-    match mod_two_eq_zero_or_one x with
-    | Or.inl mod2_eq =>
-      rw [←div_add_mod x 2] at xnz
-      simp only [mod2_eq, ne_eq, Nat.mul_eq_zero, Nat.add_zero, false_or] at xnz
-      have ⟨d, dif⟩   := hyp x_pos xnz
-      apply Exists.intro (d+1)
-      simp_all
-    | Or.inr mod2_eq =>
-      apply Exists.intro 0
-      simp_all
+  induction x using binaryRecFromOne with
+  | z₀ => exact absurd rfl xnz
+  | z₁ => exact ⟨0, rfl⟩
+  | f b n n0 hyp =>
+    obtain ⟨i, h⟩ := hyp n0
+    refine ⟨i + 1, ?_⟩
+    rwa [testBit_succ, bit_div_two]
 
 theorem ne_implies_bit_diff {x y : Nat} (p : x ≠ y) : ∃ i, testBit x i ≠ testBit y i := by
-  induction y using Nat.div2Induction generalizing x with
-  | ind y hyp =>
-    cases Nat.eq_zero_or_pos y with
-    | inl yz =>
-      simp only [yz, Nat.zero_testBit, Bool.eq_false_iff]
-      simp only [yz] at p
-      have ⟨i,ip⟩  := ne_zero_implies_bit_true p
-      apply Exists.intro i
-      simp [ip]
-    | inr ypos =>
-      if lsb_diff : x % 2 = y % 2 then
-        rw [←Nat.div_add_mod x 2, ←Nat.div_add_mod y 2] at p
-        simp only [ne_eq, lsb_diff, Nat.add_right_cancel_iff,
-          Nat.zero_lt_succ, Nat.mul_left_cancel_iff] at p
-        have ⟨i, ieq⟩  := hyp ypos p
-        apply Exists.intro (i+1)
-        simpa
-      else
-        apply Exists.intro 0
-        simp only [testBit_zero]
-        revert lsb_diff
-        cases mod_two_eq_zero_or_one x with | _ p =>
-          cases mod_two_eq_zero_or_one y with | _ q =>
-            simp [p,q]
+  induction y using binaryRec' generalizing x with
+  | z =>
+    simp only [zero_testBit, Bool.ne_false_iff]
+    exact ne_zero_implies_bit_true p
+  | f yb y h hyp =>
+    rw [← x.bit_decomp] at *
+    by_cases hb : testBit x 0 = yb
+    · subst hb
+      obtain ⟨i, h⟩ := hyp (mt (congrArg _) p)
+      refine ⟨i + 1, ?_⟩
+      rwa [testBit_succ, bit_div_two, testBit_succ, bit_div_two]
+    · refine ⟨0, ?_⟩
+      simpa using hb
 
 /--
 `eq_of_testBit_eq` allows proving two natural numbers are equal
@@ -139,25 +134,18 @@ theorem eq_of_testBit_eq {x y : Nat} (pred : ∀i, testBit x i = testBit y i) :
     have p := pred i
     contradiction
 
-theorem ge_two_pow_implies_high_bit_true {x : Nat} (p : x ≥ 2^n) : ∃ i, i ≥ n ∧ testBit x i := by
-  induction x using div2Induction generalizing n with
-  | ind x hyp =>
-    have x_pos : x > 0 := Nat.lt_of_lt_of_le (Nat.two_pow_pos n) p
-    have x_ne_zero : x ≠ 0 := Nat.ne_of_gt x_pos
+theorem ge_two_pow_implies_high_bit_true {x : Nat} (p : 2^n ≤ x) : ∃ i, n ≤ i ∧ testBit x i := by
+  induction x using binaryRec generalizing n with
+  | z => exact absurd p (Nat.not_le_of_lt n.two_pow_pos)
+  | f xb x hyp =>
     match n with
-    | zero =>
-      let ⟨j, jp⟩ := ne_zero_implies_bit_true x_ne_zero
-      exact Exists.intro j (And.intro (Nat.zero_le _) jp)
-    | succ n =>
-      have x_ge_n : x / 2 ≥ 2 ^ n := by
-          simpa [le_div_iff_mul_le, ← Nat.pow_succ'] using p
-      have ⟨j, jp⟩ := @hyp x_pos n x_ge_n
-      apply Exists.intro (j+1)
-      apply And.intro
-      case left =>
-        exact (Nat.succ_le_succ jp.left)
-      case right =>
-        simpa using jp.right
+    | 0 =>
+      simp only [zero_le, true_and]
+      exact ne_zero_implies_bit_true (ne_of_gt (Nat.lt_of_succ_le p))
+    | n+1 =>
+      obtain ⟨i, h⟩ := hyp (mul_two_le_bit.mp p)
+      refine ⟨i + 1, ?_⟩
+      rwa [Nat.add_le_add_iff_right, testBit_succ, bit_div_two]
 
 theorem testBit_implies_ge {x : Nat} (p : testBit x i = true) : x ≥ 2^i := by
   simp only [testBit_to_div_mod] at p
@@ -181,8 +169,6 @@ theorem lt_pow_two_of_testBit (x : Nat) (p : ∀i, i ≥ n → testBit x i = fal
   have test_false := p _ i_ge_n
   simp only [test_true] at test_false
 
-/-! ### testBit -/
-
 private theorem succ_mod_two : succ x % 2 = 1 - x % 2 := by
   induction x with
   | zero =>
@@ -226,7 +212,7 @@ theorem testBit_two_pow_add_gt {i j : Nat} (j_lt_i : j < i) (x : Nat) :
     rw [Nat.sub_eq_zero_iff_le] at i_sub_j_eq
     exact Nat.not_le_of_gt j_lt_i i_sub_j_eq
   | d+1 =>
-    simp [Nat.pow_succ, Nat.mul_comm _ 2,  Nat.mul_add_mod]
+    simp [Nat.pow_succ, Nat.mul_comm _ 2, Nat.mul_add_mod]
 
 @[simp] theorem testBit_mod_two_pow (x j i : Nat) :
     testBit (x % 2^j) i = (decide (i < j) && testBit x i) := by
@@ -250,7 +236,7 @@ theorem testBit_two_pow_add_gt {i j : Nat} (j_lt_i : j < i) (x : Nat) :
             exact Nat.lt_add_of_pos_right (Nat.two_pow_pos j)
       simp only [hyp y y_lt_x]
       if i_lt_j : i < j then
-        rw [ Nat.add_comm _ (2^_), testBit_two_pow_add_gt i_lt_j]
+        rw [Nat.add_comm _ (2^_), testBit_two_pow_add_gt i_lt_j]
       else
         simp [i_lt_j]
 
@@ -265,9 +251,7 @@ theorem testBit_two_pow_sub_succ (h₂ : x < 2 ^ n) (i : Nat) :
     match n with
     | 0 => simp
     | n+1 =>
-      -- just logic + omega:
-      simp only [zero_lt_succ, decide_True, Bool.true_and]
-      rw [← decide_not, decide_eq_decide]
+      simp [← decide_not]
       omega
   | succ i ih =>
     simp only [testBit_succ]
@@ -481,3 +465,34 @@ theorem mul_add_lt_is_or {b : Nat} (b_lt : b < 2^i) (a : Nat) : 2^i * a + b = 2^
 
 @[simp] theorem testBit_shiftRight (x : Nat) : testBit (x >>> i) j = testBit x (i+j) := by
   simp [testBit, ←shiftRight_add]
+
+theorem bit_shiftRight_one (b n) : bit b n >>> 1 = n :=
+  bit_div_two b n
+
+/-! ### binaryRec -/
+
+@[simp]
+theorem binaryRec_zero {C : Nat → Sort u} (z : C 0) (f : ∀ b n, C n → C (bit b n)) :
+    binaryRec z f 0 = z :=
+  rfl
+
+theorem binaryRec_of_ne_zero {C : Nat → Sort u} (z : C 0) (f : ∀ b n, C n → C (bit b n)) {n}
+    (h : n ≠ 0) :
+    binaryRec z f n = bit_decomp n ▸ f (n.testBit 0) (n >>> 1) (binaryRec z f (n >>> 1)) := by
+  rw [binaryRec, dif_neg h, eqRec_eq_cast, eqRec_eq_cast]; rfl
+
+theorem binaryRec_eq {C : Nat → Sort u} {z : C 0} {f : ∀ b n, C n → C (bit b n)} (b n)
+    (h : f false 0 z = z ∨ (n = 0 → b = true)) :
+    binaryRec z f (bit b n) = f b n (binaryRec z f n) := by
+  by_cases h' : bit b n = 0
+  case pos =>
+    obtain ⟨rfl, rfl⟩ := bit_eq_zero_iff.mp h'
+    simp only [forall_const, or_false] at h
+    exact h.symm
+  case neg =>
+    rw [binaryRec_of_ne_zero _ _ h']
+    generalize bit_decomp (bit b n) = e; revert e
+    rw [bit_testBit_zero, bit_shiftRight_one]
+    intros; rfl
+
+end Nat
diff --git a/src/Init/Data/Nat/Lemmas.lean b/src/Init/Data/Nat/Lemmas.lean
index 85d51cc2e4d0..b0c73bd2d69c 100644
--- a/src/Init/Data/Nat/Lemmas.lean
+++ b/src/Init/Data/Nat/Lemmas.lean
@@ -585,6 +585,7 @@ protected theorem mul_lt_mul_of_lt_of_lt {a b c d : Nat} (hac : a < c) (hbd : b
 
 theorem succ_mul_succ (a b) : succ a * succ b = a * b + a + b + 1 := by
   rw [succ_mul, mul_succ]; rfl
+
 theorem mul_le_add_right (m k n : Nat) : k * m ≤ m + n ↔ (k-1) * m ≤ n := by
   match k with
   | 0 =>
@@ -681,11 +682,6 @@ theorem mul_div_le (m n : Nat) : n * (m / n) ≤ m := by
   | _, Or.inl rfl => rw [Nat.zero_mul]; exact m.zero_le
   | n, Or.inr h => rw [Nat.mul_comm, ← Nat.le_div_iff_mul_le h]; exact Nat.le_refl _
 
-theorem mod_two_eq_zero_or_one (n : Nat) : n % 2 = 0 ∨ n % 2 = 1 :=
-  match n % 2, @Nat.mod_lt n 2 (by decide) with
-  | 0, _ => .inl rfl
-  | 1, _ => .inr rfl
-
 theorem le_of_mod_lt {a b : Nat} (h : a % b < a) : b ≤ a :=
   Nat.not_lt.1 fun hf => (ne_of_lt h).elim (Nat.mod_eq_of_lt hf)
 
@@ -731,6 +727,14 @@ theorem mul_mod (a b n : Nat) : a * b % n = (a % n) * (b % n) % n := by
 theorem add_mod (a b n : Nat) : (a + b) % n = ((a % n) + (b % n)) % n := by
   rw [add_mod_mod, mod_add_mod]
 
+@[simp]
+theorem mod_two_ne_one {n : Nat} : ¬n % 2 = 1 ↔ n % 2 = 0 := by
+  cases mod_two_eq_zero_or_one n with | _ h => simp [h]
+
+@[simp]
+theorem mod_two_ne_zero {n : Nat} : ¬n % 2 = 0 ↔ n % 2 = 1 := by
+  cases mod_two_eq_zero_or_one n with | _ h => simp [h]
+
 /-! ### pow -/
 
 theorem pow_succ' {m n : Nat} : m ^ n.succ = m * m ^ n := by
diff --git a/tests/lean/run/binrec.lean b/tests/lean/run/binrec.lean
index ab329c80d66e..6d66c3963a02 100644
--- a/tests/lean/run/binrec.lean
+++ b/tests/lean/run/binrec.lean
@@ -1,13 +1,13 @@
-def Nat.bit (b : Bool) (n : Nat) : Nat :=
+def Nat.bit' (b : Bool) (n : Nat) : Nat :=
   cond b (2*n+1) (2*n)
 
-theorem Nat.bit_div_even (h : n % 2 = 0) : bit false (n / 2) = n := by
-  simp [bit]
+theorem Nat.bit'_div_even (h : n % 2 = 0) : bit' false (n / 2) = n := by
+  simp [bit']
   have := Nat.div_add_mod n 2
   simp [h] at this
   assumption
 
-theorem Nat.bit_div_odd (h : n % 2 ≠ 0) : bit true (n / 2) = n := by
+theorem Nat.bit'_div_odd (h : n % 2 ≠ 0) : bit' true (n / 2) = n := by
   have h : n % 2 = 1 := by
     have := mod_lt n (by decide : 2 > 0)
     revert h this
@@ -16,7 +16,7 @@ theorem Nat.bit_div_odd (h : n % 2 ≠ 0) : bit true (n / 2) = n := by
     | 0   => decide
     | 1   => decide
     | n+2 => intros; contradiction
-  simp [bit]
+  simp [bit']
   have := Nat.div_add_mod n 2
   simp [h] at this
   assumption
@@ -36,21 +36,21 @@ theorem Nat.div2_lt (h : n ≠ 0) : n / 2 < n := by
 def Nat.binrec
     (motive : Nat → Sort u)
     (base : Unit → motive 0)
-    (ind  : (b : Bool) → (n : Nat) → (Unit → motive n) → motive (bit b n))
+    (ind  : (b : Bool) → (n : Nat) → (Unit → motive n) → motive (bit' b n))
     (n : Nat) : motive n :=
   if h₁ : n = 0 then
     h₁ ▸ base ()
   else if h₂ : n % 2 = 0 then
-    bit_div_even h₂ ▸ ind false (n / 2) (fun _ => binrec motive base ind (n / 2))
+    bit'_div_even h₂ ▸ ind false (n / 2) (fun _ => binrec motive base ind (n / 2))
   else
-    bit_div_odd h₂ ▸ ind true  (n / 2) (fun _ => binrec motive base ind (n / 2))
+    bit'_div_odd h₂ ▸ ind true  (n / 2) (fun _ => binrec motive base ind (n / 2))
 termination_by n
 decreasing_by all_goals exact Nat.div2_lt h₁
 
 theorem Nat.binind
     (motive : Nat → Prop)
     (base : motive 0)
-    (ind  : (b : Bool) → (n : Nat) → motive n → motive (bit b n))
+    (ind  : (b : Bool) → (n : Nat) → motive n → motive (bit' b n))
     (n : Nat) : motive n :=
  binrec motive (fun _ => base) (fun b n ih => ind b n (ih ())) n