feat: de-mathlib Nat.binaryRec

Std/Data/Nat/Basic.lean

@@ -127,6 +127,15 @@ where
       guess
 termination_by iter guess => guess
 
+/-!
+### 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
+
 /-- `bodd n` returns `true` if `n` is odd-/
 def bodd (n : Nat) : Bool :=
   (1 &&& n) != 0
@@ -215,3 +224,11 @@ def binaryRecFromOne {C : Nat → Sort u} (z₀ : C 0) (z₁ : C 1)
       rw [h', h h']
       exact z₁
     else f b n h' ih
+/-!
+### 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

Std/Data/Nat/Lemmas.lean

@@ -346,10 +346,20 @@ theorem succ_eq_one_add (n) : succ n = 1 + n := (one_add _).symm
 theorem succ_add_eq_add_succ (a b) : succ a + b = a + succ b := Nat.succ_add ..
 @[deprecated] alias succ_add_eq_succ_add := Nat.succ_add_eq_add_succ
 
-protected theorem add_eq_zero {n m : Nat} : n + m = 0 ↔ n = 0 ∧ m = 0 :=
-  ⟨eq_zero_of_add_eq_zero, by simp (config := {contextual := true})⟩
+theorem eq_zero_of_add_eq_zero : ∀ {n m}, n + m = 0 → n = 0 ∧ m = 0
+  | 0, 0, _ => ⟨rfl, rfl⟩
+  | _+1, 0, h => Nat.noConfusion h
 
-protected theorem add_left_cancel_iff {n m k : Nat} : n + m = n + k ↔ m = k :=
+protected theorem eq_zero_of_add_eq_zero_right (h : n + m = 0) : n = 0 :=
+  (Nat.eq_zero_of_add_eq_zero h).1
+
+protected theorem eq_zero_of_add_eq_zero_left (h : n + m = 0) : m = 0 :=
+  (Nat.eq_zero_of_add_eq_zero h).2
+
+protected theorem add_eq_zero_iff : n + m = 0 ↔ n = 0 ∧ m = 0 :=
+  ⟨Nat.eq_zero_of_add_eq_zero, fun ⟨h₁, h₂⟩ => h₂.symm ▸ h₁⟩
+
+protected theorem add_left_cancel_iff {n : Nat} : n + m = n + k ↔ m = k :=
   ⟨Nat.add_left_cancel, fun | rfl => rfl⟩
 
 protected theorem add_right_cancel_iff {n : Nat} : m + n = k + n ↔ m = k :=
@@ -955,6 +965,11 @@ 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)
 
@@ -1297,6 +1312,27 @@ theorem shiftRight_eq_div_pow (m : Nat) : ∀ n, m >>> n = m / 2 ^ n
     rw [shiftRight_add, shiftRight_eq_div_pow m k]
     simp [Nat.div_div_eq_div_mul, ← Nat.pow_succ]
 
+theorem mul_add_div {m : Nat} (m_pos : m > 0) (x y : Nat) : (m * x + y) / m = x + y / m := by
+  match x with
+  | 0 => simp
+  | x + 1 =>
+    simp [Nat.mul_succ, Nat.add_assoc _ m,
+          mul_add_div m_pos x (m+y),
+          div_eq (m+y) m,
+          m_pos,
+          Nat.le_add_right m, Nat.add_succ, Nat.succ_add]
+
+theorem mul_add_mod (m x y : Nat) : (m * x + y) % m = y % m := by
+  match x with
+  | 0 => simp
+  | x + 1 =>
+    simp [Nat.mul_succ, Nat.add_assoc _ m, mul_add_mod _ x]
+
+@[simp] theorem mod_div_self (m n : Nat) : m % n / n = 0 := by
+  cases n
+  · exact (m % 0).div_zero
+  · case succ n => exact Nat.div_eq_of_lt (m.mod_lt n.succ_pos)
+
 /-! ### shiftLeft -/
 
 theorem shiftLeft_zero (m) : m <<< 0 = m := rfl