noncomputable def Nat.find! (p : ℕ → Prop) : ℕ

Equations

• Nat.find! p = if h : ∃ (n : ℕ), p n ∧ ∀ k < n, ¬p k then h.choose else 0

@[irreducible]

def Nat.powTwo (n : ℕ) : Bool

Equations

• n.powTwo = if n = 1 then true else if n = 0 ∨ Odd n then false else (n / 2).powTwo

def Nat.chkLe (n : ℕ) (p : ℕ → Bool) : Bool

Equations

• Nat.chkLe 0 p = (p 0 && true)
• n_2.succ.chkLe p = (p n_2.succ && n_2.chkLe p)

def Nat.chkLt (n : ℕ) (p : ℕ → Bool) : Bool

Equations

• Nat.chkLt 0 p = true
• n_2.succ.chkLt p = n_2.chkLe p

noncomputable def Nat.ofProp (p : Prop) : ℕ

Equations

• Nat.ofProp p = if p then 1 else 0

theorem Nat.rec_const (n m : ℕ) : rec m (fun (x a : ℕ) => a) n = m

theorem Nat.rec_succ' {α : Type u_1} {z : α} (f : ℕ → α → α) {n : ℕ} : rec z f (n + 1) = rec (f 0 z) (fun (m : ℕ) => f (m + 1)) n

theorem Nat.infi_eq_zero_of {f : ℕ → ℕ} (k : ℕ) (h : f k = 0) : ⨅ (x : ℕ), f x = 0

theorem Nat.le_sub_add_of {a b c : ℕ} (h : a ≤ b) : a ≤ b - c + c

theorem Nat.le_sub_add_add_of {a b c d : ℕ} (h : a ≤ b) : a ≤ b - c + d + c

theorem Nat.rec_le_of_sub_sub {n z : ℕ} (f g : ℕ → ℕ) : rec z (fun (k x : ℕ) => x - f k - g k) n ≤ rec z (fun (k x : ℕ) => x - f k) n

@[simp]

theorem Nat.ite_11_iff {P Q : Prop} {h₁ : Decidable P} {h₂ : Decidable Q} : ((if P then 1 else 0) = if Q then 1 else 0) ↔ (P ↔ Q)

@[simp]

theorem Nat.ite_00_iff {P Q : Prop} {h₁ : Decidable P} {h₂ : Decidable Q} : ((if P then 0 else 1) = if Q then 0 else 1) ↔ (P ↔ Q)

@[simp]

theorem Nat.ite_10_iff {P Q : Prop} {h₁ : Decidable P} {h₂ : Decidable Q} : ((if P then 1 else 0) = if Q then 0 else 1) ↔ (P ↔ ¬Q)

@[simp]

theorem Nat.ite_01_iff {P Q : Prop} {h₁ : Decidable P} {h₂ : Decidable Q} : ((if P then 0 else 1) = if Q then 1 else 0) ↔ (P ↔ ¬Q)

theorem Nat.rec_sub {n k m : ℕ} {f : ℕ → ℕ} : rec (n - k) (fun (k a : ℕ) => a - f k) m = rec n (fun (k a : ℕ) => a - f k) m - k

@[simp]

theorem Nat.add_succ_max_ne_left {x a b : ℕ} : x + (max a b + 1) ≠ a

@[simp]

theorem Nat.add_succ_max_ne_right {x a b : ℕ} : x + (max a b + 1) ≠ b

@[simp]

theorem Nat.left_lt_succ_max {a b : ℕ} : a < max a b + 1

@[simp]

theorem Nat.right_lt_succ_max {a b : ℕ} : b < max a b + 1

theorem Nat.add_add_sub_cancel {a b c : ℕ} : a + b + c - b = a + c

theorem Nat.add_succ_ne_right {a b : ℕ} : a + (b + 1) ≠ b

theorem Nat.fn_set_add {a b : ℕ} {f : ℕ → ℕ} {x : ℕ} : fn_set a (f a + b) f x = f x + if x = a then b else 0

theorem Nat.eq_add_of_sub_eq_succ {a b c : ℕ} (h : a - b = c + 1) : a = c + 1 + b

theorem Nat.eq_add_iff_sub_eq_succ {a b c : ℕ} : a = c + 1 + b ↔ a - b = c + 1

theorem Nat.eq_add_of_one_eq_sub {a b : ℕ} (h : 1 = a - b) : a = b + 1

theorem Nat.one_eq_sub_iff {a b : ℕ} : 1 = a - b ↔ a = b + 1

@[simp]

theorem Nat.not_lt_sub {a b : ℕ} : ¬a < a - b

theorem Nat.sub_eq_left_iff {a b : ℕ} : a - b = a ↔ a = 0 ∨ b = 0

@[simp]

theorem Nat.ite_10_le_one {P : Prop} [Decidable P] : (if P then 1 else 0) ≤ 1

@[simp]

theorem Nat.ite_01_le_one {P : Prop} [Decidable P] : (if P then 0 else 1) ≤ 1

theorem Nat.even_iff_exi {n : ℕ} : Even n ↔ ∃ (k : ℕ), n = k * 2

theorem Nat.odd_iff_exi {n : ℕ} : Odd n ↔ ∃ (k : ℕ), n = k * 2 + 1

theorem Nat.mod_2_ind {p : ℕ → Prop} (h₁ : ∀ (n : ℕ), p (n * 2)) (h₂ : ∀ (n : ℕ), p (n * 2 + 1)) (n : ℕ) : p n

theorem Nat.not_even_mul_2_succ {n : ℕ} : ¬Even (n * 2 + 1)

@[simp]

theorem Nat.not_odd_mul_2 {n : ℕ} : ¬Odd (n * 2)

@[simp]

theorem Nat.even_succ_iff {n : ℕ} : Even (n + 1) ↔ Odd n

@[simp]

theorem Nat.odd_succ_iff {n : ℕ} : Odd (n + 1) ↔ Even n

theorem Nat.even_of_succ_div_2_eq {n : ℕ} (h : (n + 1) / 2 = n / 2) : Even n

theorem Nat.odd_of_succ_div_2_eq {n : ℕ} (h : (n + 1) / 2 = n / 2 + 1) : Odd n

theorem Nat.le_one_iff {n : ℕ} : n ≤ 1 ↔ n = 0 ∨ n = 1

theorem Nat.of_between_succ {a b : ℕ} (h₁ : a ≤ b) (h₂ : b ≤ a + 1) : b = a ∨ b = a + 1

theorem Nat.succ_div_2_eq_or_eq (n : ℕ) : (n + 1) / 2 = n / 2 ∨ (n + 1) / 2 = n / 2 + 1

@[simp]

theorem Nat.succ_div_2_eq_div_iff {n : ℕ} : (n + 1) / 2 = n / 2 ↔ Even n

@[simp]

theorem Nat.succ_div_2_eq_div_iff' {n : ℕ} : n / 2 = (n + 1) / 2 ↔ Even n

@[simp]

theorem Nat.succ_div_2_eq_div_succ_iff {n : ℕ} : (n + 1) / 2 = n / 2 + 1 ↔ Odd n

@[simp]

theorem Nat.succ_div_2_eq_div_succ_iff' {n : ℕ} : n / 2 + 1 = (n + 1) / 2 ↔ Odd n

@[simp]

theorem Nat.mul_2_succ_div_2_eq (n : ℕ) : (n * 2 + 1) / 2 = n

theorem Nat.find!_eq {p : ℕ → Prop} : find! p = if h : ∃ (n : ℕ), p n then Nat.find h else 0

theorem Nat.find!_spec' {p : ℕ → Prop} (h : ∃ (n : ℕ), p n) : p (find! p) ∧ ∀ (k : ℕ), p k → find! p ≤ k

theorem Nat.find!_spec {p : ℕ → Prop} (h : ∃ (n : ℕ), p n) : p (find! p)

theorem Nat.find!_eq_of {p : ℕ → Prop} {n : ℕ} (h₁ : p n) (h₂ : ∀ k < n, ¬p k) : find! p = n

theorem Nat.find!_eq_zero_of {p : ℕ → Prop} (h : ∀ (n : ℕ), ¬p n) : find! p = 0

theorem Nat.find!_eq_iff {p : ℕ → Prop} {n : ℕ} : find! p = n ↔ if ∃ (n : ℕ), p n then p n ∧ ∀ k < n, ¬p k else n = 0

theorem Nat.find!_min {p : ℕ → Prop} {n : ℕ} (h : n < find! p) : ¬p n

theorem Nat.find!_eq_of_not_ap_zero {p : ℕ → Prop} (h₁ : ∃ (n : ℕ), p n) (h₂ : ¬p 0) : find! p = (find! fun (m : ℕ) => p (m + 1)) + 1

theorem Nat.find!_eq_of_not_ap_le {p : ℕ → Prop} (n : ℕ) (h₁ : ∃ (n : ℕ), p n) (h₂ : ∀ k ≤ n, ¬p k) : find! p = (find! fun (m : ℕ) => p (n + m)) + n

theorem Nat.add_one_add {a b : ℕ} : a + 1 + b = a + b + 1

theorem Nat.add_one_sub {a b : ℕ} (h : b ≤ a) : a + 1 - b = a - b + 1

theorem Nat.le_exp_left {a b : ℕ} (h : 2 ≤ b) : a ≤ b ^ a

theorem Nat.le_exp_right {a b : ℕ} (h : b ≠ 0) : a ≤ a ^ b

theorem Nat.find_le_find_of_imp {P Q : ℕ → Prop} [hp : DecidablePred P] [hq : DecidablePred Q] {h₁ : ∃ (n : ℕ), P n} {h₂ : ∃ (n : ℕ), Q n} (h₃ : ∀ (n : ℕ), Q n → P n) : Nat.find h₁ ≤ Nat.find h₂

@[simp]

theorem Nat.le_self_mul_iff {a b : ℕ} : a ≤ a * b ↔ a = 0 ∨ b ≠ 0

@[simp]

theorem Nat.lt_self_add_iff {a b : ℕ} : a < a + b ↔ 0 < b

@[simp]

theorem Nat.div_mul_sub_one_le {n k : ℕ} : n / k * (k - 1) ≤ n / k * k

@[simp]

theorem Nat.div_mul_le_self' {m n : ℕ} : m / n * n ≤ m

@[simp]

theorem Nat.mod_add_div₁ {m k : ℕ} : m % k + k * (m / k) = m

@[simp]

theorem Nat.mod_add_div₂ {m k : ℕ} : m % k + m / k * k = m

@[simp]

theorem Nat.div_add_mod₁ {m k : ℕ} : k * (m / k) + m % k = m

@[simp]

theorem Nat.div_add_mod₂ {m k : ℕ} : m / k * k + m % k = m

theorem Nat.div_mul_le_of_le {a b c : ℕ} (h : c ≤ b) : a / b * c ≤ a

theorem Nat.add_sub_lt_add_of_sub_lt {a b c d : ℕ} (h : b - c < d) : a + b - c < a + d

theorem Nat.mod_self_sub_one_eq_one {n : ℕ} (h : 3 ≤ n) : n % (n - 1) = 1

theorem Nat.ne_zero_of_mod_ne_zero {n k : ℕ} (h : n % k ≠ 0) : n ≠ 0

@[simp]

theorem Nat.even_or_odd₁ {n : ℕ} : Even n ∨ Odd n

@[simp]

theorem Nat.odd_or_even₁ {n : ℕ} : Odd n ∨ Even n

theorem Nat.ite_odd {α : Type u_1} {n : ℕ} {x y : α} : (if Odd n then x else y) = if Even n then y else x

theorem Nat.ite_even {α : Type u_1} {n : ℕ} {x y : α} : (if Even n then x else y) = if Odd n then y else x

theorem Nat.exi_least_of_exi {p : ℕ → Prop} (h : ∃ (n : ℕ), p n) : ∃ (n : ℕ), p n ∧ ∀ k < n, ¬p k

theorem Nat.exi_iff_exi_least {p : ℕ → Prop} : (∃ (n : ℕ), p n) ↔ ∃ (n : ℕ), p n ∧ ∀ k < n, ¬p k

@[simp]

theorem Nat.le_self_sub_add_one_iff {a b : ℕ} : a ≤ a - (b + 1) ↔ a = 0

theorem Nat.find!_pos_of {p : ℕ → Prop} (h₁ : ¬p 0) (h₂ : ∃ (n : ℕ), p n) : 0 < find! p

theorem Nat.odd_add_two {n : ℕ} : Odd (n + 2) ↔ Odd n

theorem Nat.even_add_two {n : ℕ} : Even (n + 2) ↔ Even n

@[simp]

theorem Nat.odd_sub_one_iff {n : ℕ} : Odd (n - 1) ↔ n ≠ 0 ∧ Even n

@[simp]

theorem Nat.even_sub_one_iff {n : ℕ} : Even (n - 1) ↔ n = 0 ∨ Odd n

theorem Nat.mul_div_mul {a b c : ℕ} (hb : b ≠ 0) : a * b / (b * c) = a / c

@[simp]

theorem Nat.mul_div_mul_succ {a b c : ℕ} : a * (b + 1) / ((b + 1) * c) = a / c

theorem Nat.one_le_of_odd {n : ℕ} (h : Odd n) : 1 ≤ n

@[simp]

theorem Nat.fn_max_zero : max 0 = id

@[simp]

theorem Nat.odd_two_pow_iff {n : ℕ} : Odd (2 ^ n) ↔ n = 0

@[simp]

theorem Nat.powTwo_eq_true_iff {n : ℕ} : n.powTwo = true ↔ ∃ (k : ℕ), 2 ^ k = n

@[simp]

theorem Nat.powTwo_eq_false_iff {n : ℕ} : n.powTwo = false ↔ ∀ (k : ℕ), 2 ^ k ≠ n

@[instance_reducible]

instance Nat.instDecidableExistsEqHPowOfNat_projects {n : ℕ} : Decidable (∃ (k : ℕ), 2 ^ k = n)

Equations

• Nat.instDecidableExistsEqHPowOfNat_projects = decidable_of_iff' (n.powTwo = true) ⋯

@[instance_reducible]

instance Nat.instDecidableForallNeHPowOfNat_projects {n : ℕ} : Decidable (∀ (k : ℕ), 2 ^ k ≠ n)

Equations

• Nat.instDecidableForallNeHPowOfNat_projects = decidable_of_iff' ((!n.powTwo) = true) ⋯

@[simp]

theorem Nat.chkLe_eq_true_iff {n : ℕ} {p : ℕ → Bool} : n.chkLe p = true ↔ ∀ k ≤ n, p k = true

@[simp]

theorem Nat.chkLe_eq_false_iff {n : ℕ} {p : ℕ → Bool} : n.chkLe p = false ↔ ∃ k ≤ n, (!p k) = true

@[simp]

theorem Nat.chkLt_eq_true_iff {n : ℕ} {p : ℕ → Bool} : n.chkLt p = true ↔ ∀ k < n, p k = true

@[simp]

theorem Nat.chkLt_eq_false_iff {n : ℕ} {p : ℕ → Bool} : n.chkLt p = false ↔ ∃ k < n, (!p k) = true

@[instance_reducible]

instance Nat.instDecidableForallForallLe_projects {n : ℕ} {p : ℕ → Prop} [h : (k : ℕ) → Decidable (p k)] : Decidable (∀ k ≤ n, p k)

Equations

• Nat.instDecidableForallForallLe_projects = decidable_of_iff' ((n.chkLe fun (b : ℕ) => decide (p b)) = true) ⋯

@[instance_reducible]

instance Nat.instDecidableExistsAndLe_projects {n : ℕ} {p : ℕ → Prop} [h : (k : ℕ) → Decidable (p k)] : Decidable (∃ k ≤ n, p k)

Equations

• Nat.instDecidableExistsAndLe_projects = decidable_of_iff' ((!n.chkLe fun (x : ℕ) => !decide (p x)) = true) ⋯

@[instance_reducible]

instance Nat.instDecidableForallForallLt_projects {n : ℕ} {p : ℕ → Prop} [h : (k : ℕ) → Decidable (p k)] : Decidable (∀ k < n, p k)

Equations

• Nat.instDecidableForallForallLt_projects = decidable_of_iff' ((n.chkLt fun (b : ℕ) => decide (p b)) = true) ⋯

@[instance_reducible]

instance Nat.instDecidableExistsAndLt_projects {n : ℕ} {p : ℕ → Prop} [h : (k : ℕ) → Decidable (p k)] : Decidable (∃ k < n, p k)

Equations

• Nat.instDecidableExistsAndLt_projects = decidable_of_iff' ((!n.chkLt fun (x : ℕ) => !decide (p x)) = true) ⋯

@[simp]

theorem Nat.mul_two_lor_mul_two {n m : ℕ} : n * 2 ||| m * 2 = (n ||| m) * 2

@[simp]

theorem Nat.mul_two_succ_lor_mul_two {n m : ℕ} : n * 2 + 1 ||| m * 2 = (n ||| m) * 2 + 1

@[simp]

theorem Nat.mul_two_lor_mul_two_succ {n m : ℕ} : n * 2 ||| m * 2 + 1 = (n ||| m) * 2 + 1

@[simp]

theorem Nat.mul_two_succ_lor_mul_two_succ {n m : ℕ} : n * 2 + 1 ||| m * 2 + 1 = (n ||| m) * 2 + 1

@[simp]

theorem Nat.odd_lor_iff {n m : ℕ} : Odd (n ||| m) ↔ Odd n ∨ Odd m

@[simp]

theorem Nat.even_lor_iff {n m : ℕ} : Even (n ||| m) ↔ Even n ∧ Even m

@[simp]

theorem Nat.even_shiftLeft_succ {n k : ℕ} : Even (n <<< (k + 1))

@[simp]

theorem Nat.not_odd_shiftLeft_succ {n k : ℕ} : ¬Odd (n <<< (k + 1))

@[simp]

theorem Nat.forall_even_shiftRight_iff {n : ℕ} : (∀ (k : ℕ), Even (n >>> k)) ↔ n = 0

theorem Nat.shiftRight_add' {n m k : ℕ} : n >>> (m + k) = n >>> k >>> m

@[simp]

theorem Nat.mul_two_add_one_div_two {n : ℕ} : (n * 2 + 1) / 2 = n

theorem Nat.div_two_eq_shiftRight {n : ℕ} : n / 2 = n >>> 1

theorem Nat.eq_iff_odd_shiftRight {n m : ℕ} : n = m ↔ ∀ (k : ℕ), Odd (n >>> k) ↔ Odd (m >>> k)

@[simp]

theorem Nat.shiftRight_add_left {n m : ℕ} : n >>> (m + n) = 0

@[simp]

theorem Nat.shiftRight_add_right {n m : ℕ} : n >>> (n + m) = 0

theorem Nat.div_mul_eq_div_div {n m k : ℕ} : n / (m * k) = n / m / k

@[simp]

theorem Nat.mul_two_add_one_div_two_pow_succ {n m : ℕ} : (n * 2 + 1) / 2 ^ (m + 1) = n / 2 ^ m

@[simp]

theorem Nat.mul_two_add_one_shiftRight_succ {n m : ℕ} : (n * 2 + 1) >>> (m + 1) = n >>> m

@[simp]

theorem Nat.lor_one_shiftRight_succ {n m : ℕ} : (n ||| 1) >>> (m + 1) = n >>> (m + 1)

@[simp]

theorem Nat.mul_two_shiftRight_succ {n m : ℕ} : (n * 2) >>> (m + 1) = n >>> m

theorem Nat.lor_one_eq_ite {n : ℕ} : n ||| 1 = if Odd n then n else n + 1

@[simp]

theorem Nat.mul_two_lor_one_eq {n : ℕ} : n * 2 ||| 1 = n * 2 + 1

@[simp]

theorem Nat.mul_two_add_one_lor_one_eq {n : ℕ} : n * 2 + 1 ||| 1 = n * 2 + 1

theorem Nat.mod_self_pow_succ {n m : ℕ} (hn : n ≠ 1) (hm : m ≠ 0) : n % n ^ (m + 1) = n

theorem Nat.beq_eq_eq {n m : ℕ} : (n == m) = decide (n = m)

theorem Nat.mod_two_eq_one_iff_odd {n : ℕ} : n % 2 = 1 ↔ Odd n

theorem Nat.mod_two_eq_zero_iff_even {n : ℕ} : n % 2 = 0 ↔ Even n

theorem Nat.testBit_eq_odd {n i : ℕ} : n.testBit i = decide (Odd (n >>> i))

theorem Nat.ne_zero_of_odd {n : ℕ} (h : Odd n) : n ≠ 0

theorem Nat.pos_of_odd {n : ℕ} (h : Odd n) : 0 < n

@[simp]

theorem Nat.sum_min_left {n m : ℕ} : n - min n m = n - m

@[simp]

theorem Nat.sum_min_right {n m : ℕ} : n - min m n = n - m

theorem Nat.eq_div_mod (n k : ℕ) : n = n / k * k + n % k

theorem Nat.eq_mod_div (n k : ℕ) : n = n % k + n / k * k

theorem Nat.eq_of_mod_eq_mod {n m : ℕ} (k : ℕ) (hn : n < k) (hm : m < k) (h : n % k = m % k) : n = m

theorem Nat.ind_step (k : ℕ) {p : ℕ → Prop} (h₁ : ∀ n < k, p n) (h₂ : ∀ (n : ℕ), (∀ c < n + k, p c) → p (n + k)) (n : ℕ) : p n

theorem Nat.not_le_mod {n k : ℕ} (hk : k ≠ 0) : ¬k ≤ n % k

@[simp]

theorem Nat.sub_succ_div_self_eq_zero {n m : ℕ} : (n - (m + 1)) / n = 0

theorem Nat.exi_mul_add (n b : ℕ) (h : b ≠ 0) : ∃ (m : ℕ), ∃ r < b, n = m * b + r

theorem Nat.lt_self_mul_add_iff {a b c : ℕ} : a < a * b + c ↔ (a ≠ 0 ∨ c ≠ 0) ∧ (a ≠ 0 → (b = 0 → a < c) ∧ (b ≠ 0 → c = 0 → b ≠ 1))

@[simp]

theorem Nat.lt_self_mul_iff' {b n : ℕ} : n < n * b ↔ 2 ≤ b ∧ n ≠ 0

@[simp]

theorem Nat.lt_mul_self_iff' {b n : ℕ} : n < b * n ↔ 2 ≤ b ∧ n ≠ 0

theorem Nat.eq_of_le_and_dvd {n b : ℕ} (hb : b ≠ 0) (hn : n ≠ 0) (h₁ : n ≤ b) (h₂ : b ∣ n) : n = b

theorem Nat.eq_of_le_and_mod_eq_zero {n b : ℕ} (hb : b ≠ 0) (hn : n ≠ 0) (h₁ : n ≤ b) (h₂ : n % b = 0) : n = b

@[simp]

theorem Nat.not_prime_0 : ¬Prime 0

@[simp]

theorem Nat.not_prime_1 : ¬Prime 1

@[simp]

theorem Nat.prime_2 : Prime 2

theorem Nat.prime_add_prime_iff {p : ℕ → ℕ → ℕ → Prop} (hp : ∀ (a b c : ℕ), p a b c ↔ p b a c) : (∀ (a b c : ℕ), Prime a → Prime b → Prime c → a + b = c → p a b c) ↔ ∀ (a c : ℕ), Prime a → Prime c → Odd a → a + 2 = c → p a 2 c

theorem Nat.three_dvd_add_two_four {n : ℕ} : 3 ∣ n ∨ 3 ∣ n + 2 ∨ 3 ∣ n + 4

theorem Nat.prime_iff' {n : ℕ} : Prime n ↔ 2 ≤ n ∧ ∀ (k : ℕ), 2 ≤ k → k < n → ¬k ∣ n

theorem Nat.eq_of_prime_and_dvd {n p : ℕ} (hp : Prime p) (hn : Prime n) (h : p ∣ n) : n = p

@[simp]

theorem Nat.one_shiftLeft_eq_one_iff {n : ℕ} : 1 <<< n = 1 ↔ n = 0

theorem Nat.ind_bit {p : ℕ → Prop} (h₁ : p 0) (h₂ : ∀ (n : ℕ), p n → p (n * 2)) (h₃ : ∀ (n : ℕ), p n → p (n * 2 + 1)) (n : ℕ) : p n

theorem Nat.or_mul_two_pow {n m k : ℕ} : (n ||| m) * 2 ^ k = n * 2 ^ k ||| m * 2 ^ k

theorem Nat.or_two_pow_eq_add_of {n k : ℕ} (h : n < 2 ^ k) : n ||| 2 ^ k = n + 2 ^ k

theorem Nat.two_pow_or_eq_add_of {n k : ℕ} (h : n < 2 ^ k) : 2 ^ k ||| n = 2 ^ k + n

theorem Nat.eq_div_add_mod (n b : ℕ) : n = n / b * b + n % b

theorem Nat.or_mul_two_pow_eq_add_of {n k c : ℕ} (h : n < 2 ^ k) : n ||| c * 2 ^ k = n + c * 2 ^ k

theorem Nat.or_two_pow_mul_eq_add_of {n k c : ℕ} (h : n < 2 ^ k) : n ||| 2 ^ k * c = n + 2 ^ k * c

@[simp]

theorem Nat.le_two_pow_self {n : ℕ} : n ≤ 2 ^ n

theorem Nat.mul_pow_mod_pow {b n k w : ℕ} : n * b ^ k % b ^ w = n % b ^ (w - k) * b ^ k

@[simp]

theorem Nat.ofProp_true : ofProp True = 1

@[simp]

theorem Nat.ofProp_false : ofProp False = 0

theorem Nat.ite_eq_ofProp {p : Prop} [Decidable p] : (if p then 1 else 0) = ofProp p

theorem Nat.ite_eq_ofProp' {p : Prop} [Decidable p] : (if p then 0 else 1) = ofProp ¬p

@[simp]

theorem Nat.ofProp_sub {p : Prop} {n : ℕ} : ofProp p - n = ofProp (n = 0 ∧ p)

@[simp]

theorem Nat.add_one_sub_ofProp {p : Prop} {n : ℕ} : n + 1 - ofProp p = n + ofProp ¬p