diff --git a/Std/Data/Nat/Basic.lean b/Std/Data/Nat/Basic.lean
index 84900593c9..c95e6390a1 100644
--- a/Std/Data/Nat/Basic.lean
+++ b/Std/Data/Nat/Basic.lean
@@ -130,11 +130,98 @@ where
       guess
 termination_by iter guess => guess
 
+/-- `bodd n` returns `true` if `n` is odd-/
+def bodd (n : Nat) : Bool :=
+  (1 &&& n) != 0 -- `1 &&& n` is faster than `n &&& 1` for big `n`. This may change in the future.
+
+/-- `div2 n = ⌊n/2⌋` the greatest integer smaller than `n/2`-/
+def div2 (n : Nat) : Nat :=
+  n >>> 1
+
+/-- `bit b` appends the digit `b` to 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
 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
+/-- `testBit m n` returns whether the `(n+1)ˢᵗ` least significant bit is `1` or `0`-/
+def testBit (m n : Nat) : Bool :=
+  bodd (m >>> n)
+
+theorem bit_val (b n) : bit b n = 2 * n + cond b 1 0 := by
+  cases b <;> rw [Nat.mul_comm]
+  · exact congrArg (· + n) n.zero_add.symm
+  · exact congrArg (· + n + 1) n.zero_add.symm
+
+theorem div2_val (n) : div2 n = 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
+
+theorem mod_two_of_bodd (n : Nat) : n % 2 = cond (bodd n) 1 0 := by
+  dsimp [bodd, (· &&& ·), AndOp.and, land]
+  unfold bitwise
+  match Nat.decEq n 0 with
+  | isTrue n0 => subst n0; decide
+  | isFalse n0 =>
+    simp only [ite_false, decide_True, Bool.true_and, decide_eq_true_eq, n0,
+      show 1 / 2 = 0 by decide]
+    cases mod_two_eq_zero_or_one n with | _ h => simp [h]; rfl
+
+theorem div2_add_bodd (n : Nat) : 2 * div2 n + cond (bodd n) 1 0 = n := by
+  rw [← mod_two_of_bodd, div2_val, Nat.div_add_mod]
+
+theorem bit_decomp (n : Nat) : bit (bodd n) (div2 n) = n :=
+  (bit_val _ _).trans (div2_add_bodd _)
+
+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.succ_add]
+
+/-- 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 _ _
+
+theorem binaryRec_decreasing (h : n ≠ 0) : div2 n < n :=
+  div_lt_self (n.zero_lt_of_ne_zero h) (by decide)
+
+/-- 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 n.bodd n.div2 (binaryRec z f n.div2)
+  decreasing_by exact binaryRec_decreasing 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 by
+      have : bit b n = 0 := by
+        rw [bit_eq_zero_iff]
+        cases n <;> cases b <;> simp at h <;> simp [h]
+      exact 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
diff --git a/Std/Data/Nat/Bitwise.lean b/Std/Data/Nat/Bitwise.lean
index 9a9fb8263b..927e7df137 100644
--- a/Std/Data/Nat/Bitwise.lean
+++ b/Std/Data/Nat/Bitwise.lean
@@ -19,6 +19,9 @@ namespace Nat
 @[local simp]
 private theorem one_div_two : 1/2 = 0 := by trivial
 
+private theorem decide_mod_two_eq_one {x : Nat} : decide (x % 2 = 1) = (x % 2 != 0) := by
+  cases mod_two_eq_zero_or_one x with | _ h => simp (config := {decide := true}) [h]
+
 private theorem two_pow_succ_sub_one_div : (2 ^ (n+1) - 1) / 2 = 2^n - 1 := by
   apply fun x => (Nat.sub_eq_of_eq_add x).symm
   apply Eq.trans _
@@ -34,21 +37,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
@@ -56,79 +44,58 @@ noncomputable def div2Induction {motive : Nat → Sort u}
   unfold bitwise
   simp
 
-@[simp] theorem and_one_is_mod (x : Nat) : x &&& 1 = x % 2 := by
+@[simp] theorem one_and_is_mod (x : Nat) : 1 &&& x = 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]
+    cases mod_two_eq_zero_or_one x with | _ p => simp [xz, p]
 
 /-! ### testBit -/
 
 @[simp] theorem zero_testBit (i : Nat) : testBit 0 i = false := by
-  simp only [testBit, zero_shiftRight, zero_and, bne_self_eq_false]
+  simp only [testBit, zero_shiftRight, bodd, and_zero, bne_self_eq_false]
 
-theorem testBit_zero_is_mod2 (x : Nat) : testBit x 0 = decide (x % 2 = 1) := by
-  cases mod_two_eq_zero_or_one x with | _ p => simp [testBit, p]
+theorem testBit_zero_is_bodd (x : Nat) : testBit x 0 = bodd x :=
+  rfl
 
-theorem testBit_succ_div2 (x i : Nat) : testBit x (succ i) = testBit (x/2) i := by
+theorem testBit_succ_div_two (x i : Nat) : testBit x (i + 1) = testBit (x / 2) i := by
   unfold testBit
-  simp [shiftRight_succ_inside]
+  simp [shiftRight_succ_inside, div2]
 
 theorem testBit_to_div_mod {x : Nat} : testBit x i = decide (x / 2^i % 2 = 1) := by
   induction i generalizing x with
   | zero =>
     unfold testBit
-    cases mod_two_eq_zero_or_one x with | _ xz => simp [xz]
+    cases mod_two_eq_zero_or_one x with | _ xz => simp [bodd, xz]
   | succ i hyp =>
-    simp [testBit_succ_div2, hyp,
+    simp [testBit_succ_div_two, hyp,
           Nat.div_div_eq_div_mul, Nat.pow_succ, Nat.mul_comm 2]
 
 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 [testBit_succ_div2, dif]
-    | Or.inr mod2_eq =>
-      apply Exists.intro 0
-      simp [testBit_zero_is_mod2, mod2_eq]
+  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_div_two, 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)
-        simp [testBit_succ_div2]
-        exact ieq
-      else
-        apply Exists.intro 0
-        simp only [testBit_zero_is_mod2]
-        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 : bodd x = yb
+    · subst hb
+      obtain ⟨i, h⟩ := hyp (ne_of_apply_ne _ p)
+      refine ⟨i + 1, ?_⟩
+      rwa [testBit_succ_div_two, bit_div_two, testBit_succ_div_two, bit_div_two]
+    · refine ⟨0, ?_⟩
+      rwa [testBit_zero_is_bodd, testBit_zero_is_bodd, bodd_bit, bodd_bit]
 
 /--
 `eq_of_testBit_eq` allows proving two natural numbers are equal
@@ -142,27 +109,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.pow_two_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.pow_two_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
-          simp [le_div_iff_mul_le, ← Nat.pow_succ']
-          exact 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 =>
-        simp [testBit_succ_div2 _ j]
-        exact 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_div_two, 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
@@ -229,7 +187,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 [pow_succ, Nat.mul_comm _ 2,  Nat.mul_add_mod]
+    simp [pow_succ, Nat.mul_comm _ 2, Nat.mul_add_mod]
 
 theorem testBit_mod_two_pow (x j i : Nat) :
     testBit (x % 2^j) i = (decide (i < j) && testBit x i) := by
@@ -262,14 +220,14 @@ private theorem testBit_one_zero : testBit 1 0 = true := by trivial
 @[simp] theorem testBit_two_pow_sub_one (n i : Nat) : testBit (2^n-1) i = decide (i < n) := by
   induction i generalizing n with
   | zero =>
-    simp [testBit_zero_is_mod2]
+    simp [testBit_zero_is_bodd]
     match n with
     | 0 =>
       simp
     | n+1 =>
-      simp [Nat.pow_succ, Nat.mul_comm _ 2, two_mul_sub_one, Nat.pow_two_pos]
+      simp [bodd, Nat.pow_succ, Nat.mul_comm _ 2, two_mul_sub_one, Nat.pow_two_pos]
   | succ i hyp =>
-    simp [testBit_succ_div2]
+    simp [testBit_succ_div_two]
     match n with
     | 0 =>
       simp [pow_zero]
@@ -304,12 +262,12 @@ theorem testBit_bitwise
       simp only [x_zero, y_zero, ←Nat.two_mul]
       cases i with
       | zero =>
-        cases p : f (decide (x % 2 = 1)) (decide (y % 2 = 1)) <;>
-          simp [p, testBit_zero_is_mod2, Nat.mul_add_mod, mod_eq_of_lt]
+        cases p : f (x % 2 != 0) (y % 2 != 0) <;>
+          simp [p, testBit_zero_is_bodd, bodd, decide_mod_two_eq_one, Nat.mul_add_mod]
       | succ i =>
         have hyp_i := hyp i (Nat.le_refl (i+1))
-        cases p : f (decide (x % 2 = 1)) (decide (y % 2 = 1)) <;>
-          simp [p, testBit_succ_div2, one_div_two, hyp_i, Nat.mul_add_div]
+        cases p : f (x % 2 != 0) (y % 2 != 0) <;>
+          simp [p, testBit_succ_div_two, decide_mod_two_eq_one, hyp_i, Nat.mul_add_div]
 
 /-! ### bitwise -/
 
diff --git a/Std/Data/Nat/Lemmas.lean b/Std/Data/Nat/Lemmas.lean
index e80ddba9c5..78f2370a66 100644
--- a/Std/Data/Nat/Lemmas.lean
+++ b/Std/Data/Nat/Lemmas.lean
@@ -5,7 +5,8 @@ Authors: Leonardo de Moura, Jeremy Avigad, Mario Carneiro
 -/
 import Std.Logic
 import Std.Tactic.Basic
-import Std.Tactic.Alias
+import Std.Tactic.RCases
+import Std.Data.Bool
 import Std.Data.Nat.Init.Lemmas
 import Std.Data.Nat.Basic
 import Std.Data.Ord
@@ -1002,11 +1003,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)
 
@@ -1084,6 +1080,31 @@ 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 one_mod (n : Nat) : 1 % (n + 2) = 1 :=
+  Nat.mod_eq_of_lt (succ_lt_succ n.succ_pos)
+
+@[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]
+
+@[simp]
+theorem mod_two_add_succ_mod_two (n : Nat) : n % 2 + (n + 1) % 2 = 1 := by
+  rw [add_mod]
+  cases mod_two_eq_zero_or_one n with | _ h => simp [h]
+
+@[simp]
+theorem succ_mod_two_add_mod_two (n : Nat) : (n + 1) % 2 + n % 2 = 1 := by
+  rw [Nat.add_comm, mod_two_add_succ_mod_two]
+
+theorem succ_mod_two_eq_one_sub_mod_two (n : Nat) : (n + 1) % 2 = 1 - n % 2 := by
+  rw [add_mod]
+  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
@@ -1359,3 +1380,115 @@ theorem mul_add_mod (m x y : Nat) : (m * x + y) % m = y % m := by
   cases n
   · exact (m % 0).div_zero
   · case succ n => exact Nat.div_eq_of_lt (m.mod_lt n.succ_pos)
+
+/-! ### 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]
+
+/-! ### bodd -/
+
+@[simp]
+theorem bodd_zero : bodd 0 = false :=
+  rfl
+
+theorem bodd_one : bodd 1 = true :=
+  rfl
+
+theorem bodd_two : bodd 2 = false :=
+  rfl
+
+theorem bodd_eq_mod_two_bne_zero (n : Nat) : bodd n = (n % 2 != 0) := by
+  rw [mod_two_of_bodd]
+  cases bodd n with | false | true => rfl
+
+@[simp]
+theorem bodd_succ (n : Nat) : bodd (succ n) = not (bodd n) := by
+  simp only [bodd_eq_mod_two_bne_zero, succ_eq_add_one, succ_mod_two_eq_one_sub_mod_two]
+  cases mod_two_eq_zero_or_one n with | _ h => simp (config := {decide := true}) [h]
+
+@[simp]
+theorem bodd_add (m n : Nat) : bodd (m + n) = ((bodd m).xor (bodd n)) := by
+  induction n with
+  | zero => simp
+  | succ n ih => simp [add_succ, ih, Bool.xor_not]
+
+@[simp]
+theorem bodd_mul (m n : Nat) : bodd (m * n) = (bodd m && bodd n) := by
+  induction n with
+  | zero => simp
+  | succ n ih =>
+    simp [mul_succ, ih]
+    cases bodd m <;> cases bodd n <;> rfl
+
+theorem bodd_bit (b n) : bodd (bit b n) = b := by
+  rw [bit_val, Nat.mul_comm, Nat.add_comm, bodd_add, bodd_mul]
+  cases b <;> cases bodd n <;> rfl
+
+/-! ### div2 -/
+
+@[simp]
+theorem div2_zero : div2 0 = 0 :=
+  rfl
+
+theorem div2_one : div2 1 = 0 :=
+  rfl
+
+theorem div2_two : div2 2 = 1 :=
+  rfl
+
+theorem div2_eq_div_two (n : Nat) : div2 n = n / 2 := rfl
+
+@[simp]
+theorem div2_succ (n : Nat) : div2 (succ n) = cond (bodd n) (succ (div2 n)) (div2 n) := by
+  apply Nat.eq_of_mul_eq_mul_left (by decide : 0 < 2)
+  apply Nat.add_right_cancel (m := cond (bodd (succ n)) 1 0)
+  rw (config := {occs := .pos [1]}) [div2_add_bodd, bodd_succ, ← div2_add_bodd n]
+  cases bodd n <;> simp [succ_eq_add_one, Nat.add_comm 1, Nat.mul_add]
+
+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
+
+theorem div2_bit (b n) : div2 (bit b n) = n :=
+  bit_div_two b n
+
+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]
+
+/-! ### binary rec/cases -/
+
+@[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.bodd n.div2 (binaryRec z f n.div2) := by
+  rw [binaryRec, dif_neg h, eqRec_eq_cast, eqRec_eq_cast]
+
+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 [bodd_bit, div2_bit]
+    intros; rfl