def Auto.Nat.beq_refl' (a : Nat) : a.beq a = true

A version of Nat.beq_refl that reduces to Eq.refl

Equations

• ⋯ = ⋯

theorem Auto.Nat.lt_of_ble_eq_false {pos : Nat} {n : Nat} : n.ble pos = false → pos < n

theorem Auto.Nat.ble_eq_false_of_lt {pos : Nat} (n : Nat) : pos < n → n.ble pos = false

theorem Auto.Nat.ble_eq_false_eq_lt {pos : Nat} (n : Nat) : (pos < n) = (n.ble pos = false)

theorem Auto.Nat.beq_eq_false_of_ne {m n : Nat} (H : m ≠ n) : m.beq n = false

theorem Auto.Nat.ne_of_beq_eq_false {m n : Nat} (H : m.beq n = false) : m ≠ n

theorem Auto.Nat.ble_add (a b e : Nat) : a.ble b = (a + e).ble (b + e)

theorem Auto.Nat.zero_ble (b : Nat) : Nat.ble 0 b = true

theorem Auto.Nat.tricotomy {m n : Nat} : m < n ∨ m = n ∨ m > n

theorem Auto.Nat.dichotomy {m n : Nat} : m ≤ n ∨ m > n

theorem Auto.Nat.lt_or_gt_of_ne {m n : Nat} (H : m ≠ n) : m < n ∨ m > n

theorem Auto.Nat.eq_of_le_of_lt_succ {n m : Nat} (h₁ : n ≤ m) (h₂ : m < n + 1) : m = n

theorem Auto.Nat.one_add (n : Nat) : 1 + n = n.succ

theorem Auto.Nat.pred_sub (n m : Nat) : n.pred - m = (n - m).pred

theorem Auto.Nat.le_max_iff (m n k : Nat) : k ≤ max m n ↔ k ≤ m ∨ k ≤ n

theorem Auto.Nat.lt_eq_succ_le {m n : Nat} : n < m ↔ n.succ ≤ m

theorem Auto.Nat.gt_eq_succ_le {m n : Nat} : m > n ↔ n.succ ≤ m

theorem Auto.Nat.le_pred_of_succ_le {n m : Nat} : m > 0 → n.succ ≤ m → n ≤ m.pred

theorem Auto.Nat.pred_lt_iff_le {n m : Nat} : m > 0 → (n.pred < m ↔ n ≤ m)

theorem Auto.Nat.max_add {a b c : Nat} : max a b + c = max (a + c) (b + c)

theorem Auto.Nat.max_lt {a b c : Nat} : max a b < c ↔ a < c ∧ b < c

theorem Auto.Nat.max_zero_left {a : Nat} : max 0 a = a

theorem Auto.Nat.max_zero_right {a : Nat} : max a 0 = a

theorem Auto.Nat.max_assoc {b c a : Nat} : max a (max b c) = max (max a b) c

theorem Auto.Nat.zero_lt_of_ne_zero {n : Nat} (h : n ≠ 0) : n > 0

theorem Auto.Nat.ne_zero_of_zero_lt {n : Nat} (h : n > 0) : n ≠ 0

theorem Auto.Nat.eq_zero_of_mul_right_lt {b a : Nat} (h : a * b < a) : b = 0

theorem Auto.Nat.eq_zero_of_mul_left_lt {b a : Nat} (h : b * a < a) : b = 0

theorem Auto.Nat.le_iff_div_eq_zero {a b : Nat} (h : b > 0) : a / b = 0 ↔ a < b

theorem Auto.Nat.le_pow {b a : Nat} (h : b ≥ 2) : a < b ^ a

theorem Auto.Nat.mod_par {a b c : Nat} (h : a % b = c) : ∃ (d : Nat), a = b * d + c

theorem Auto.Nat.div_par {a b c : Nat} (h : a / b = c) (hnz : b > 0) : ∃ (d : Nat), a = b * c + d ∧ d < b

theorem Auto.Nat.le_par {a b : Nat} (h : a ≤ b) : ∃ (c : Nat), b = a + c

theorem Auto.Nat.lt_par {a b : Nat} (h : a < b) : ∃ (c : Nat), b = a + 1 + c

theorem Auto.Nat.sub_mod (a b n : Nat) (h : a ≥ b) : (a - b) % n = (a - b % n) % n

theorem Auto.Nat.testBit_true_iff (a i : Nat) : a.testBit i = true ↔ 2 ^ i ≤ a % 2 ^ (i + 1)

theorem Auto.Nat.testBit_false_iff (a i : Nat) : a.testBit i = false ↔ a % 2 ^ (i + 1) < 2 ^ i

theorem Auto.Nat.ones_testBit_true_of_lt (n i : Nat) (h : i < n) : (2 ^ n - 1).testBit i = true

theorem Auto.Nat.ones_testBit_false_of_ge (n i : Nat) (h : i ≥ n) : (2 ^ n - 1).testBit i = false

theorem Auto.Nat.xor_def (a b : Nat) : a ^^^ b = a.xor b

theorem Auto.Nat.ones_xor (n a : Nat) (h : a < 2 ^ n) : 2 ^ n - 1 ^^^ a = 2 ^ n - 1 - a