ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>x n : Nat<VAR>h₁ : n ≤ x<VAR>h₂ : x < 2 * n<GOAL>x % n = x - n
<VAR>n : Nat<VAR>a b : Fin n<GOAL>↑(a - b) = ↑a - ↑b ↔ b ≤ a
<VAR>n : Nat<VAR>a b : Fin n<GOAL>↑(a - b) = n + ↑a - ↑b ↔ a < b
<VAR>n : Nat<VAR>a b : Fin n<GOAL>↑(a * b) = ↑a * ↑b % n
<VAR>n : Nat<VAR>k : Fin (n + 1)<GOAL>k * 1 = k
<VAR>n : Nat<VAR>a b : Fin n<GOAL>a * b = b * a
<VAR>n : Nat<VAR>a b c : Fin n<GOAL>a * b * c = a * (b * c)
<VAR>n : Nat<VAR>k : Fin (n + 1)<GOAL>1 * k = k
<VAR>n : Nat<VAR>k : Fin (n + 1)<GOAL>k * 0 = 0
<VAR>n : Nat<VAR>k : Fin (n + 1)<GOAL>0 * k = 0
<VAR>a b : Int<GOAL>(a ∣ b) = ∃ c, b = a * c
<VAR>a b c : Int<GOAL>a ∣ b → b ∣ c → a ∣ c
<VAR>m n : Nat<GOAL>↑m ∣ ↑n ↔ m ∣ n
<VAR>a b : Int<VAR>H1 : 0 ≤ a<VAR>H2 : 0 ≤ b<GOAL>a ∣ b → b ∣ a → a = b
<VAR>n : Int<GOAL>0 ∣ n ↔ n = 0
<VAR>a b : Int<GOAL>-a ∣ b ↔ a ∣ b
<VAR>a b : Int<GOAL>a ∣ -b ↔ a ∣ b
<VAR>a b : Int<GOAL>a.natAbs ∣ b.natAbs ↔ a ∣ b
<VAR>n : Nat<VAR>z : Int<GOAL>↑n ∣ z ↔ n ∣ z.natAbs
<VAR>a b c : Int<GOAL>a ∣ b → a ∣ c → a ∣ b + c
<VAR>a b c : Int<GOAL>a ∣ b → a ∣ c → a ∣ b - c
<VAR>a b c : Int<VAR>H : a ∣ c<GOAL>a ∣ b + c ↔ a ∣ b
<VAR>a b c : Int<VAR>H : a ∣ b<GOAL>a ∣ b + c ↔ a ∣ c
<VAR>a b c : Int<VAR>H : a ∣ b - c<GOAL>a ∣ b ↔ a ∣ c
<VAR>a b c : Int<VAR>H : a ∣ b + c<GOAL>a ∣ b ↔ a ∣ c
<VAR>a b : Int<VAR>bpos : 0 < b<VAR>H : a ∣ b<GOAL>a ≤ b
<VAR>a b : Int<GOAL>↑a.natAbs ∣ b ↔ a ∣ b
<VAR>a b : Int<GOAL>a ∣ ↑b.natAbs ↔ a ∣ b
<VAR>a : Int<GOAL>↑a.natAbs ∣ a
<VAR>a : Int<GOAL>a ∣ ↑a.natAbs
<VAR>n : Nat<VAR>z : Int<GOAL>z ∣ ↑n ↔ z.natAbs ∣ n
<VAR>a : Int<VAR>H : 0 ≤ a<VAR>H' : a ∣ 1<GOAL>a = 1
<VAR>a b : Int<VAR>H : 0 ≤ a<VAR>H' : a * b = 1<GOAL>a = 1
<VAR>a b : Int<VAR>H : 0 ≤ b<VAR>H' : a * b = 1<GOAL>b = 1
<VAR>b : Int<GOAL>Int.div 0 b = 0
<VAR>b : Int<GOAL>Int.fdiv 0 b = 0
<VAR>a : Int<GOAL>a.fdiv 0 = 0
<VAR>a b : Int<GOAL>0 ≤ a → 0 ≤ b → a.div b = a / b
<VAR>a : Int<VAR>b : Int<GOAL>0 ≤ b → a.fdiv b = a / b
<VAR>a b : Int<VAR>Ha : 0 ≤ a<VAR>Hb : 0 ≤ b<GOAL>a.fdiv b = a.div b
<VAR>b : Int<GOAL>Int.mod 0 b = 0
<VAR>b : Int<GOAL>Int.fmod 0 b = 0
<VAR>m n : Nat<GOAL>↑(m % n) = ↑m % ↑n
<VAR>m n : Nat<GOAL>↑n - (↑m % ↑n + 1) - (↑n * (↑m / ↑n) + ↑n) = -[m+1]
<VAR>a b : Int<GOAL>a % b + b * (a / b) = a
<VAR>a b : Int<GOAL>a % b + a / b * b = a
<VAR>a b : Int<GOAL>b * (a / b) + a % b = a
<VAR>a b : Int<GOAL>a / b * b + a % b = a
<VAR>a b : Int<GOAL>a % b = a - b * (a / b)
<VAR>a b : Int<GOAL>a.mod b + b * a.div b = a
<VAR>a b : Int<GOAL>b * a.div b + a.mod b = a
<VAR>m k : Int<GOAL>m.mod k + m.div k * k = m
<VAR>m k : Int<GOAL>m.div k * k + m.mod k = m
<VAR>a b : Int<GOAL>a.mod b = a - b * a.div b
<VAR>a b : Int<GOAL>a.fmod b + b * a.fdiv b = a
<VAR>a b : Int<GOAL>b * a.fdiv b + a.fmod b = a
<VAR>a b : Int<GOAL>a.fmod b = a - b * a.fdiv b
<VAR>a : Int<VAR>b : Int<VAR>hb : 0 ≤ b<GOAL>a.fmod b = a % b
<VAR>a b : Int<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<GOAL>a.mod b = a % b
<VAR>a b : Int<VAR>Ha : 0 ≤ a<VAR>Hb : 0 ≤ b<GOAL>a.fmod b = a.mod b
<VAR>a b : Int<GOAL>a / -b = -(a / b)
<VAR>a b : Int<VAR>Ha : a < 0<VAR>Hb : 0 < b<GOAL>a / b < 0
<VAR>a b : Int<GOAL>a / b = a.ediv b
<VAR>m : Nat<VAR>b : Int<VAR>H : 0 < b<GOAL>-[m+1] / b = -((↑m).div b + 1)
<VAR>a b : Int<VAR>Ha : 0 ≤ a<VAR>Hb : 0 ≤ b<GOAL>0 ≤ a / b
<VAR>a b : Int<VAR>Ha : 0 ≤ a<VAR>Hb : b ≤ 0<GOAL>a / b ≤ 0
<VAR>a b : Int<VAR>c : Int<VAR>H : c ≠ 0<GOAL>(a + b * c) / c = a / c + b
<VAR>a b c : Int<VAR>H : c ∣ b<GOAL>(a + b) / c = a / c + b / c
<VAR>a b c : Int<VAR>H : c ∣ a<GOAL>(a + b) / c = a / c + b / c
<VAR>a : Int<VAR>b : Int<VAR>H : b ≠ 0<GOAL>a * b / b = a
<VAR>a : Int<VAR>b : Int<VAR>H : a ≠ 0<GOAL>a * b / a = b
<VAR>a b : Int<VAR>h : 0 < b<GOAL>a / b ≥ 0 ↔ a ≥ 0
<VAR>a b : Int<VAR>H1 : 0 ≤ a<VAR>H2 : a < b<GOAL>a / b = 0
<VAR>a : Int<VAR>b : Int<VAR>c : Int<VAR>H : b ≠ 0<GOAL>(a + b * c) / b = a / b + c
<VAR>a : Int<VAR>b c : Int<VAR>H : 0 < a<GOAL>a * b / (a * c) = b / c
<VAR>a : Int<VAR>b : Int<VAR>c : Int<VAR>H : 0 < b<GOAL>a * b / (c * b) = a / c
<VAR>a b c : Int<VAR>H1 : b ≠ 0<VAR>H2 : a = b * c<GOAL>a / b = c
<VAR>a b c : Int<VAR>H1 : a ≠ 0<VAR>H2 : a * b = c<GOAL>b = c / a
<VAR>a b c : Int<VAR>H1 : b ≠ 0<VAR>H2 : a = c * b<GOAL>a / b = c
<VAR>m n : Int<GOAL>m % n = m.emod n
<VAR>m : Nat<VAR>b : Int<VAR>bpos : 0 < b<GOAL>-[m+1] % b = b - 1 - ↑m % b
<VAR>m : Nat<VAR>n : Int<GOAL>-[m+1] % n = Int.subNatNat n.natAbs (m % n.natAbs).succ
<VAR>m n : Nat<GOAL>↑m % ↑n = ↑(m % n)
<VAR>a : Int<VAR>b : Int<GOAL>b ≠ 0 → 0 ≤ a % b
<VAR>a : Int<VAR>b : Int<VAR>H : 0 < b<GOAL>a % b < b
<VAR>x k : Int<VAR>h : k ≠ 0<GOAL>k * (x / k) ≤ x
<VAR>x k : Int<VAR>h : 0 < k<GOAL>x < k * (x / k) + k
<VAR>a b c : Int<GOAL>(a + b * c) % c = a % c
<VAR>a b c : Int<GOAL>(a + b * c) % b = a % b
<VAR>a b : Int<GOAL>(a + b) % b = a % b
<VAR>a b : Int<GOAL>(a + b) % a = b % a
<VAR>a b : Int<GOAL>-a % b = (b - a) % b
<VAR>m n k : Int<GOAL>(m % n + k) % n = (m + k) % n
<VAR>m n k : Int<GOAL>(m + n % k) % k = (m + n) % k
<VAR>a b n : Int<GOAL>(a + b) % n = (a % n + b % n) % n
<VAR>m n k : Int<VAR>i : Int<VAR>H : m % n = k % n<GOAL>(m + i) % n = (k + i) % n
<VAR>m n k : Int<VAR>i : Int<GOAL>(m + i) % n = (k + i) % n ↔ m % n = k % n
<VAR>a b n : Int<GOAL>a * b % n = a % n * (b % n) % n
<VAR>n : Int<VAR>m k : Int<VAR>h : m ∣ k<GOAL>n % k % m = n % m
<VAR>a b : Int<GOAL>a % b % b = a % b
<VAR>a b n : Int<GOAL>(a - b) % n = (a % n - b % n) % n
<VAR>a b : Int<VAR>H1 : 0 ≤ a<VAR>H2 : a < b<GOAL>a % b = a
<VAR>x : Int<VAR>h : 0 ≤ x<GOAL>x % (x + 1) = x
<VAR>a b : Int<VAR>H : a % b = 0<GOAL>b * (a / b) = a
<VAR>a b : Int<VAR>H : a % b = 0<GOAL>a / b * b = a
<VAR>x : Int<GOAL>x % 2 = 0 ∨ x % 2 = 1
<VAR>m n k : Int<VAR>i : Int<VAR>H : m % n = k % n<GOAL>(i + m) % n = (i + k) % n
<VAR>m n k i : Int<GOAL>(i + m) % n = (i + k) % n ↔ m % n = k % n
<VAR>m n k : Int<VAR>i : Int<GOAL>(m - i) % n = (k - i) % n ↔ m % n = k % n
<VAR>m n k : Int<GOAL>m % n = k % n ↔ (m - k) % n = 0
<VAR>a b r q : Int<VAR>h : 0 < b<GOAL>a / b = q ∧ a % b = r ↔ r + b * q = a ∧ 0 ≤ r ∧ r < b
<VAR>a : Int<VAR>b c : Int<VAR>H : 0 < a<GOAL>a * b % (a * c) = a * (b % c)
<VAR>a : Int<VAR>b : Int<VAR>H : 0 < b<GOAL>a < (a / b + 1) * b
<VAR>a : Int<VAR>n : Nat<GOAL>(a / ↑n).natAbs ≤ a.natAbs
<VAR>a b : Int<GOAL>(a / b).natAbs ≤ a.natAbs
<VAR>a : Int<VAR>b : Int<VAR>Ha : 0 ≤ a<GOAL>a / b ≤ a
<VAR>a b : Int<VAR>H : b % a = 0<GOAL>a ∣ b
<VAR>x : Int<VAR>m : Nat<GOAL>↑m ∣ x % ↑m - x
<VAR>a b : Int<GOAL>a ∣ b → b % a = 0
<VAR>a b : Int<GOAL>a ∣ b ↔ b % a = 0
<VAR>a b : Int<VAR>h : ¬a ∣ b<GOAL>a = 0 ∨ 0 < b % a
<VAR>a : Int<VAR>b c : Int<GOAL>c ∣ b → a * b / c = a * (b / c)
<VAR>b : Int<VAR>a c : Int<VAR>h : c ∣ a<GOAL>a * b / c = a / c * b
<VAR>a b : Int<GOAL>b ∣ a → -a / b = -(a / b)
<VAR>a : Int<VAR>b c : Int<VAR>hcb : c ∣ b<GOAL>(a - b) / c = a / c - b / c
<VAR>a : Int<VAR>H : a ≠ 0<GOAL>a / a = 1
<VAR>x y : Int<GOAL>(x - y) % y = x % y
<VAR>a b c : Int<VAR>h : a % b = c<GOAL>b ∣ a - c
<VAR>a b : Int<VAR>H : b ∣ a<GOAL>a / b * b = a
<VAR>a b : Int<VAR>H : a ∣ b<GOAL>a * (b / a) = b
<VAR>a b c : Int<VAR>H1 : b ∣ a<VAR>H2 : a / b = c<GOAL>a = b * c
<VAR>a b c : Int<VAR>H : b ≠ 0<VAR>H' : b ∣ a<GOAL>a / b = c ↔ a = b * c
<VAR>a b c : Int<VAR>H : b ≠ 0<VAR>H' : b ∣ a<GOAL>a / b = c ↔ a = c * b
<VAR>a b c : Int<VAR>H1 : b ∣ a<VAR>H2 : a / b = c<GOAL>a = c * b
<VAR>d n : Int<VAR>h : d ∣ n<VAR>H : n / d = 0<GOAL>n = 0
<VAR>a b c : Int<VAR>hcab : c ∣ a - b<GOAL>(a - b) / c = a / c - b / c
<VAR>a b d : Int<VAR>hda : d ∣ a<VAR>hdb : d ∣ b<GOAL>a / d = b / d ↔ a = b
<VAR>a b : Int<GOAL>a / b.sign = a * b.sign
<VAR>a : Int<VAR>b : Int<VAR>H : b ≠ 0<GOAL>a / b * b ≤ a
<VAR>a b c : Int<VAR>w : a * b ≤ a * c<VAR>h : 0 < a<GOAL>b ≤ c
<VAR>a b c : Int<VAR>w : b * a ≤ c * a<VAR>h : 0 < a<GOAL>b ≤ c
<VAR>a b c : Int<VAR>H : 0 < c<VAR>H' : a ≤ b * c<GOAL>a / c ≤ b
<VAR>a b c : Int<VAR>H : 0 < c<VAR>H3 : a < b / c<GOAL>a * c < b
<VAR>a b c : Int<VAR>H1 : 0 < c<VAR>H2 : a ≤ b / c<GOAL>a * c ≤ b
<VAR>a b c : Int<VAR>H : 0 < c<VAR>H' : a < b * c<GOAL>a / c < b
<VAR>a b c : Int<VAR>w : a * b < a * c<VAR>h : 0 ≤ a<GOAL>b < c
<VAR>a b c : Int<VAR>w : b * a < c * a<VAR>h : 0 ≤ a<GOAL>b < c
<VAR>a b c : Int<VAR>H1 : 0 < c<VAR>H2 : a * c ≤ b<GOAL>a ≤ b / c
<VAR>a b c : Int<VAR>H : 0 < c<GOAL>a ≤ b / c ↔ a * c ≤ b
<VAR>a b c : Int<VAR>H : 0 < c<VAR>H' : a ≤ b<GOAL>a / c ≤ b / c
<VAR>a b c : Int<VAR>H1 : 0 < c<VAR>H2 : a / c < b<GOAL>a < b * c
<VAR>a b c : Int<VAR>H : 0 < c<GOAL>a / c < b ↔ a < b * c
<VAR>a b c : Int<VAR>H1 : 0 ≤ b<VAR>H2 : b ∣ a<VAR>H3 : a / b ≤ c<GOAL>a ≤ c * b
<VAR>a b c : Int<VAR>H1 : 0 ≤ b<VAR>H2 : b ∣ c<VAR>H3 : a * b < c<GOAL>a < c / b
<VAR>a b : Int<VAR>c : Int<VAR>H : 0 < c<VAR>H' : c ∣ b<GOAL>a < b / c ↔ a * c < b
<VAR>a b : Int<VAR>H1 : 0 < a<VAR>H2 : 0 ≤ b<VAR>H3 : b ∣ a<GOAL>0 < a / b
<VAR>a b c d : Int<VAR>H2 : d ∣ c<VAR>H3 : b ≠ 0<VAR>H4 : d ≠ 0<VAR>H5 : a * d = b * c<GOAL>a / b = c / d
<VAR>a b : Int<GOAL>a.div (-b) = -a.div b
<VAR>a b : Int<GOAL>(-a).div b = -a.div b
<VAR>a b : Int<GOAL>(-a).div (-b) = a.div b
<VAR>a b : Int<VAR>Ha : 0 ≤ a<VAR>Hb : 0 ≤ b<GOAL>0 ≤ a.div b
<VAR>a b : Int<VAR>Ha : 0 ≤ a<VAR>Hb : b ≤ 0<GOAL>a.div b ≤ 0
<VAR>a b : Int<VAR>H1 : 0 ≤ a<VAR>H2 : a < b<GOAL>a.div b = 0
<VAR>a : Int<VAR>b : Int<VAR>H : b ≠ 0<GOAL>(a * b).div b = a
<VAR>a : Int<VAR>b : Int<VAR>H : a ≠ 0<GOAL>(a * b).div a = b
<VAR>a : Int<VAR>H : a ≠ 0<GOAL>a.div a = 1
<VAR>a b : Int<VAR>H : a.mod b = 0<GOAL>b * a.div b = a
<VAR>a b : Int<VAR>H : a.mod b = 0<GOAL>a.div b * b = a
<VAR>a b : Int<VAR>H : b.mod a = 0<GOAL>a ∣ b
<VAR>a : Int<VAR>b c : Int<GOAL>c ∣ b → (a * b).div c = a * b.div c
<VAR>b : Int<VAR>a c : Int<VAR>h : c ∣ a<GOAL>(a * b).div c = a.div c * b
<VAR>a b c : Int<GOAL>a ∣ b → b ∣ c → b.div a ∣ c.div a
<VAR>a b : Int<GOAL>(a.div b).natAbs = a.natAbs.div b.natAbs
<VAR>a b c : Int<VAR>H1 : b ≠ 0<VAR>H2 : a = b * c<GOAL>a.div b = c
<VAR>a b c : Int<VAR>H1 : a ≠ 0<VAR>H2 : a * b = c<GOAL>b = c.div a
<VAR>m n : Nat<GOAL>↑(m % n) = (↑m).mod ↑n
<VAR>a b : Int<VAR>H1 : 0 ≤ a<VAR>H2 : a < b<GOAL>a.mod b = a
<VAR>a : Int<VAR>b : Int<VAR>H : 0 < b<GOAL>a.mod b < b
<VAR>a : Int<VAR>b : Int<GOAL>0 ≤ a → 0 ≤ a.mod b
<VAR>a b : Int<GOAL>a.mod (-b) = a.mod b
<VAR>a b : Int<GOAL>(a * b).mod b = 0
<VAR>a b : Int<GOAL>(a * b).mod a = 0
<VAR>a b : Int<GOAL>a ∣ b → b.mod a = 0
<VAR>a b : Int<GOAL>a ∣ b ↔ b.mod a = 0
<VAR>a b : Int<VAR>H : b ∣ a<GOAL>a.div b * b = a
<VAR>a b : Int<VAR>H : a ∣ b<GOAL>a * b.div a = b
<VAR>a b c : Int<VAR>H1 : b ∣ a<VAR>H2 : a.div b = c<GOAL>a = b * c
<VAR>a : Int<VAR>b : Int<VAR>H : 0 < b<GOAL>a < (a.div b + 1) * b
<VAR>a b c : Int<VAR>H : b ≠ 0<VAR>H' : b ∣ a<GOAL>a.div b = c ↔ a = b * c
<VAR>a b c : Int<VAR>H : b ≠ 0<VAR>H' : b ∣ a<GOAL>a.div b = c ↔ a = c * b
<VAR>a b c : Int<VAR>H1 : b ∣ a<VAR>H2 : a.div b = c<GOAL>a = c * b
<VAR>a b c : Int<VAR>H1 : b ≠ 0<VAR>H2 : a = c * b<GOAL>a.div b = c
<VAR>d n : Int<VAR>h : d ∣ n<VAR>H : n.div d = 0<GOAL>n = 0
<VAR>a b d : Int<VAR>hda : d ∣ a<VAR>hdb : d ∣ b<GOAL>a.div d = b.div d ↔ a = b
<VAR>a b : Int<GOAL>a.div b.sign = a * b.sign
<VAR>a : Int<GOAL>a.sign = a.div ↑a.natAbs
<VAR>a b : Int<VAR>Ha : 0 ≤ a<VAR>Hb : 0 ≤ b<GOAL>0 ≤ a.fdiv b
<VAR>a b : Int<GOAL>0 ≤ a → b ≤ 0 → a.fdiv b ≤ 0
<VAR>a b : Int<GOAL>a < 0 → 0 < b → a.fdiv b < 0
<VAR>a : Int<VAR>b : Int<VAR>H : b ≠ 0<GOAL>(a * b).fdiv b = a
<VAR>a : Int<VAR>b : Int<VAR>H : a ≠ 0<GOAL>(a * b).fdiv a = b
<VAR>a : Int<VAR>H : a ≠ 0<GOAL>a.fdiv a = 1
<VAR>a : Int<VAR>b : Int<VAR>H : 0 < b<GOAL>a < (a.fdiv b + 1) * b
<VAR>m n : Nat<GOAL>↑(m % n) = (↑m).fmod ↑n
<VAR>a : Int<GOAL>a.fmod 1 = 0
<VAR>a b : Int<VAR>H1 : 0 ≤ a<VAR>H2 : a < b<GOAL>a.fmod b = a
<VAR>a b : Int<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<GOAL>0 ≤ a.fmod b
<VAR>a : Int<VAR>b : Int<VAR>hb : 0 < b<GOAL>0 ≤ a.fmod b
<VAR>a : Int<VAR>b : Int<VAR>H : 0 < b<GOAL>a.fmod b < b
<VAR>a b : Int<GOAL>(a * b).fmod b = 0
<VAR>a b : Int<GOAL>(a * b).fmod a = 0
<VAR>a b : Int<VAR>h : b ∣ a<GOAL>a.div b = a / b
<VAR>a b : Int<GOAL>b ∣ a → a.fdiv b = a / b
<VAR>x : Int<VAR>m : Nat<GOAL>x.bmod m % ↑m = x % ↑m
<VAR>x : Int<VAR>n : Nat<GOAL>(x % ↑n).bmod n = x.bmod n
<VAR>x : Int<VAR>m : Nat<GOAL>x.bmod m = if x % ↑m < (↑m + 1) / 2 then x % ↑m else x % ↑m - ↑m
<VAR>x : Int<VAR>m : Nat<VAR>p : x % ↑m < (↑m + 1) / 2<GOAL>x.bmod m = x % ↑m
<VAR>x : Int<VAR>m : Nat<VAR>p : x % ↑m ≥ (↑m + 1) / 2<GOAL>x.bmod m = x % ↑m - ↑m
<VAR>x : Int<GOAL>x.bmod 1 = 0
<VAR>x : Int<VAR>n : Nat<GOAL>(x + ↑n).bmod n = x.bmod n
<VAR>x : Int<VAR>n : Nat<VAR>k : Int<GOAL>(x + ↑n * k).bmod n = x.bmod n
<VAR>x : Int<VAR>n : Nat<GOAL>(x - ↑n).bmod n = x.bmod n
<VAR>y : Int<VAR>x : Int<VAR>n : Nat<GOAL>(x % ↑n + y).bmod n = (x + y).bmod n
<VAR>y : Int<VAR>x : Int<VAR>n : Nat<GOAL>(x % ↑n * y).bmod n = (x * y).bmod n
<VAR>x : Int<VAR>n : Nat<VAR>y : Int<GOAL>(x.bmod n + y).bmod n = (x + y).bmod n
<VAR>x y : Int<VAR>n : Nat<GOAL>(x + y.bmod n).bmod n = (x + y).bmod n
<VAR>x : Int<VAR>n : Nat<VAR>y : Int<GOAL>(x.bmod n * y).bmod n = (x * y).bmod n
<VAR>x y : Int<VAR>n : Nat<GOAL>(x * y.bmod n).bmod n = (x * y).bmod n
<VAR>a b : Int<VAR>n : Nat<GOAL>(a + b).bmod n = (a.bmod n + b.bmod n).bmod n
<VAR>x : Int<VAR>m : Nat<GOAL>(x % ↑m).bmod m = x.bmod m
<VAR>x : Int<VAR>m : Nat<GOAL>(x.bmod m).bmod m = x.bmod m
<VAR>m : Nat<GOAL>Int.bmod 0 m = 0
<VAR>x : Int<VAR>m : Nat<GOAL>↑m ∣ x.bmod m - x
<VAR>x : Int<VAR>m : Nat<VAR>h : 0 < m<GOAL>-(↑m / 2) ≤ x.bmod m
<VAR>x : Int<VAR>m : Nat<VAR>h : 0 < m<GOAL>x.bmod m < (↑m + 1) / 2
<VAR>x : Int<VAR>m : Nat<VAR>h : 0 < m<GOAL>x.bmod m ≤ (↑m - 1) / 2
<VAR>x : Int<VAR>w : 1 < x.natAbs<GOAL>x.bmod (x.natAbs + 1) = -x.sign
<VAR>a b : Char<GOAL>a ≤ b ↔ a.val ≤ b.val
<VAR>a b : Char<GOAL>a < b ↔ a.val < b.val
<VAR>a b : Char<GOAL>¬a ≤ b ↔ b < a
<VAR>a b : Char<GOAL>¬a < b ↔ b ≤ a
<VAR>a b c : Char<GOAL>a ≤ b → b ≤ c → a ≤ c
<VAR>a b c : Char<GOAL>a < b → b < c → a < c
<VAR>a b : Char<GOAL>a ≤ b ∨ b ≤ a
<VAR>a b : Char<VAR>h : a < b<GOAL>¬b < a
<VAR>a b : Char<VAR>h : a < b<GOAL>a ≠ b
<VAR>c : Char<GOAL>c.utf8Size = 1 ∨ c.utf8Size = 2 ∨ c.utf8Size = 3 ∨ c.utf8Size = 4
<VAR>c : Char<GOAL>Char.ofNat c.toNat = c
<VAR>a b : String<VAR>h : a = b<GOAL>a.data = b.data
<VAR>a b : String<VAR>h : a.data ≠ b.data<GOAL>a ≠ b
<VAR>a b : String<VAR>h : a < b<GOAL>a ≠ b
<VAR>x y : Nat<GOAL>0 < y ∧ y ≤ x → x - y < x
<VAR>x y : Nat<GOAL>x / y = ite (0 < y ∧ y ≤ x) ((x - y) / y + 1) 0
<VAR>n k : Nat<GOAL>n / k ≤ n
<VAR>n k : Nat<VAR>hLtN : 0 < n<VAR>hLtK : 1 < k<GOAL>n / k < n
<VAR>n m : Nat<GOAL>n.modCore m = n % m
<VAR>x y : Nat<GOAL>x % y = ite (0 < y ∧ y ≤ x) ((x - y) % y) x
<VAR>a b : Nat<VAR>h : a < b<GOAL>a % b = a
<VAR>a b : Nat<VAR>h : a ≥ b<GOAL>a % b = (a - b) % b
<VAR>x : Nat<VAR>y : Nat<GOAL>y > 0 → x % y < y
<VAR>x y : Nat<GOAL>x % y ≤ x
<VAR>m n : Nat<GOAL>n * (m / n) + m % n = m
<VAR>b a : Nat<VAR>h₁ : 0 < b<VAR>h₂ : b ≤ a<GOAL>a / b = (a - b) / b + 1
<VAR>m k : Nat<GOAL>m % k + k * (m / k) = m
<VAR>k x y : Nat<VAR>k0 : 0 < k<GOAL>x ≤ y / k ↔ x * k ≤ y
<VAR>m n k : Nat<GOAL>m / n / k = m / (n * k)
<VAR>m n : Nat<GOAL>m / n * n ≤ m
<VAR>k x y : Nat<VAR>Hk : 0 < k<GOAL>x / k < y ↔ x < y * k
<VAR>x : Nat<VAR>z : Nat<VAR>H : 0 < z<GOAL>(x + z) / z = x / z + 1
<VAR>x : Nat<VAR>z : Nat<VAR>H : 0 < z<GOAL>(z + x) / z = x / z + 1
<VAR>x z : Nat<VAR>y : Nat<VAR>H : 0 < y<GOAL>(x + y * z) / y = x / y + z
<VAR>x y : Nat<VAR>z : Nat<VAR>H : 0 < z<GOAL>(x + y * z) / z = x / z + y
<VAR>x z : Nat<GOAL>(x + z) % z = x % z
<VAR>x z : Nat<GOAL>(x + z) % x = z % x
<VAR>x y z : Nat<GOAL>(x + y * z) % y = x % y
<VAR>x y z : Nat<GOAL>(x + y * z) % z = x % z
<VAR>m n : Nat<GOAL>m * n % m = 0
<VAR>m n : Nat<GOAL>m * n % n = 0
<VAR>k n m : Nat<VAR>lo : k * n ≤ m<VAR>hi : m < (k + 1) * n<GOAL>m / n = k
<VAR>x n p : Nat<VAR>h₁ : n * p ≤ x<GOAL>(x - n * p) / n = x / n - p
<VAR>x n p : Nat<VAR>h₁ : x < n * p<GOAL>(n * p - (x + 1)) / n = p - (x / n + 1)
<VAR>z x y : Nat<GOAL>z * x % (z * y) = z * (x % y)
<VAR>a b : Nat<VAR>h₀ : a < b<GOAL>a / b = 0
<VAR>m : Nat<VAR>n : Nat<VAR>H : 0 < n<GOAL>m * n / n = m
<VAR>m : Nat<VAR>n : Nat<VAR>H : 0 < n<GOAL>n * m / n = m
<VAR>m n k : Nat<GOAL>m ≤ k * n → m / k ≤ n
<VAR>n : Nat<VAR>m : Nat<VAR>H : 0 < m<GOAL>m * n / m = n
<VAR>n : Nat<VAR>H : 0 < n<GOAL>n / n = 1
<VAR>n m k : Nat<VAR>H1 : 0 < n<VAR>H2 : m = k * n<GOAL>m / n = k
<VAR>n m k : Nat<VAR>H1 : 0 < n<VAR>H2 : m = n * k<GOAL>m / n = k
<VAR>m : Nat<VAR>n k : Nat<VAR>H : 0 < m<GOAL>m * n / (m * k) = n / k
<VAR>m : Nat<VAR>n k : Nat<VAR>H : 0 < m<GOAL>n * m / (k * m) = n / k
<VAR>m n : Nat<GOAL>n * (m / n) ≤ m
<VAR>n x : Nat<GOAL>(2 ^ (n + 1) - (x + 1)) / 2 = 2 ^ n - (x / 2 + 1)
<VAR>n : Nat<GOAL>(2 ^ (n + 1) - 1) / 2 = 2 ^ n - 1
<VAR>n : Nat<VAR>n_pos : n > 0<GOAL>(2 * n - 1) % 2 = 1
<VAR>x : Nat<GOAL>x &&& 0 = 0
<VAR>n : Nat<GOAL>1 &&& n = n % 2
<VAR>x : Nat<GOAL>x &&& 1 = x % 2
<VAR>i : Nat<GOAL>Nat.testBit 0 i = false
<VAR>x : Nat<GOAL>x.testBit 0 = decide (x % 2 = 1)
<VAR>x i : Nat<GOAL>x.testBit i.succ = (x / 2).testBit i
<VAR>x i : Nat<GOAL>x.testBit (i + 1) = (x / 2).testBit i
<VAR>i x : Nat<GOAL>x.testBit i = decide (x / 2 ^ i % 2 = 1)
<VAR>x i : Nat<GOAL>(x.testBit i).toNat = x / 2 ^ i % 2
<VAR>x : Nat<VAR>xnz : x ≠ 0<GOAL>∃ i, x.testBit i = true
<VAR>x y : Nat<VAR>p : x ≠ y<GOAL>∃ i, x.testBit i ≠ y.testBit i
<VAR>x y : Nat<VAR>pred : ∀ (i : Nat), x.testBit i = y.testBit i<GOAL>x = y
<VAR>n x : Nat<VAR>p : x ≥ 2 ^ n<GOAL>∃ i, i ≥ n ∧ x.testBit i = true
<VAR>i x : Nat<VAR>p : x.testBit i = true<GOAL>x ≥ 2 ^ i
<VAR>x i : Nat<VAR>lt : x < 2 ^ i<GOAL>x.testBit i = false
<VAR>n : Nat<VAR>x : Nat<VAR>p : ∀ (i : Nat), i ≥ n → x.testBit i = false<GOAL>x < 2 ^ n
<VAR>x : Nat<GOAL>x.succ % 2 = 1 - x % 2
<VAR>x : Nat<GOAL>(x + 1).testBit 0 = !x.testBit 0
<VAR>x i : Nat<GOAL>(2 ^ i + x).testBit i = !x.testBit i
<VAR>a b i : Nat<GOAL>(2 ^ i * a + b).testBit i = (decide (a % 2 = 1)).xor (b.testBit i)
<VAR>i j : Nat<VAR>j_lt_i : j < i<VAR>x : Nat<GOAL>(2 ^ i + x).testBit j = x.testBit j
<VAR>x j i : Nat<GOAL>(x % 2 ^ j).testBit i = (decide (i < j) && x.testBit i)
<VAR>x : Nat<GOAL>(!decide (x % 2 = 1)) = decide (x % 2 = 0)
<VAR>x n : Nat<VAR>h₂ : x < 2 ^ n<VAR>i : Nat<GOAL>(2 ^ n - (x + 1)).testBit i = (decide (i < n) && !x.testBit i)
<VAR>n i : Nat<GOAL>(2 ^ n - 1).testBit i = decide (i < n)
<VAR>b : Bool<VAR>i : Nat<GOAL>b.toNat.testBit i = (decide (i = 0) && b)
<VAR>i : Nat<GOAL>Nat.testBit 1 i = true ↔ i = 0
<VAR>f : Bool → Bool → Bool<VAR>false_false_axiom : f false false = false<VAR>x y i : Nat<GOAL>(Nat.bitwise f x y).testBit i = f (x.testBit i) (y.testBit i)
<VAR>x : Nat<GOAL>x < 1 ↔ x = 0
<VAR>x : Nat<GOAL>x < 2 ^ 0 ↔ x = 0
<VAR>m n : Nat<VAR>p : m < 2 ^ n.succ<GOAL>m / 2 < 2 ^ n
<VAR>x n y : Nat<VAR>f : Bool → Bool → Bool<VAR>left : x < 2 ^ n<VAR>right : y < 2 ^ n<GOAL>Nat.bitwise f x y < 2 ^ n
<VAR>x y i : Nat<GOAL>(x &&& y).testBit i = (x.testBit i && y.testBit i)
<VAR>x : Nat<VAR>y n : Nat<VAR>right : y < 2 ^ n<GOAL>x &&& y < 2 ^ n
<VAR>x n : Nat<GOAL>x &&& 2 ^ n - 1 = x % 2 ^ n
<VAR>n x : Nat<VAR>lt : x < 2 ^ n<GOAL>x &&& 2 ^ n - 1 = x
<VAR>x y i : Nat<GOAL>(x ||| y).testBit i = (x.testBit i || y.testBit i)
<VAR>x y n : Nat<VAR>left : x < 2 ^ n<VAR>right : y < 2 ^ n<GOAL>x ||| y < 2 ^ n
<VAR>x y i : Nat<GOAL>(x ^^^ y).testBit i = (x.testBit i).xor (y.testBit i)
<VAR>x y n : Nat<VAR>left : x < 2 ^ n<VAR>right : y < 2 ^ n<GOAL>x ^^^ y < 2 ^ n
<VAR>a : Nat<VAR>b i : Nat<VAR>b_lt : b < 2 ^ i<VAR>j : Nat<GOAL>(2 ^ i * a + b).testBit j = if j < i then b.testBit j else a.testBit (j - i)
<VAR>i a j : Nat<GOAL>(2 ^ i * a).testBit j = (decide (j ≥ i) && a.testBit (j - i))
<VAR>i b : Nat<VAR>b_lt : b < 2 ^ i<VAR>a : Nat<GOAL>2 ^ i * a + b = 2 ^ i * a ||| b
<VAR>i j : Nat<VAR>x : Nat<GOAL>(x <<< i).testBit j = (decide (j ≥ i) && x.testBit (j - i))
<VAR>i j : Nat<VAR>x : Nat<GOAL>(x >>> i).testBit j = x.testBit (i + j)
<VAR>a b c d : Nat<GOAL>a + b + (c + d) = a + c + (b + d)
<VAR>n : Nat<GOAL>1 + n = n.succ
<VAR>n : Nat<GOAL>n.succ = 1 + n
<VAR>a b : Nat<GOAL>a.succ + b = a + b.succ
<VAR>n m : Nat<VAR>h : n + m = 0<GOAL>n = 0
<VAR>n m : Nat<GOAL>n + m = 0 ↔ n = 0 ∧ m = 0
<VAR>m k n : Nat<GOAL>n + m = n + k ↔ m = k
<VAR>m k n : Nat<GOAL>m + n = k + n ↔ m = k
<VAR>m k n : Nat<GOAL>n + m ≤ n + k ↔ m ≤ k
<VAR>k m n : Nat<GOAL>k + n < m + n → k < m
<VAR>k m n : Nat<GOAL>n + k < n + m → k < m
<VAR>k n m : Nat<GOAL>k + n < k + m ↔ n < m
<VAR>k n m : Nat<GOAL>n + k < m + k ↔ n < m
<VAR>a b c d : Nat<VAR>hle : a ≤ b<VAR>hlt : c < d<GOAL>a + c < b + d
<VAR>a b c d : Nat<VAR>hlt : a < b<VAR>hle : c ≤ d<GOAL>a + c < b + d
<VAR>k n : Nat<GOAL>0 < k → n < k + n
<VAR>n k : Nat<VAR>h : n < n + k<GOAL>0 < k
<VAR>n k : Nat<GOAL>n < k + n → 0 < k
<VAR>n k : Nat<GOAL>n < n + k ↔ 0 < k
<VAR>n k : Nat<GOAL>n < k + n ↔ 0 < k
<VAR>m : Nat<VAR>h : 0 < m<VAR>n : Nat<GOAL>0 < m + n
<VAR>n : Nat<VAR>m : Nat<VAR>h : 0 < n<GOAL>0 < m + n
<VAR>n : Nat<GOAL>n + n ≠ 1
<VAR>n : Nat<GOAL>n - 1 = n.pred
<VAR>n : Nat<GOAL>1 - n = if n = 0 then 1 else 0
<VAR>n m k : Nat<GOAL>n.succ - m - k.succ = n - m - k
<VAR>n m k l : Nat<GOAL>n + l - m - (k + l) = n - m - k
<VAR>m n k : Nat<GOAL>m - n - k = m - k - n
<VAR>n m : Nat<VAR>h : m ≤ n<GOAL>m + (n - m) = n
<VAR>n : Nat<GOAL>n.succ - 1 = n
<VAR>n : Nat<GOAL>n + 1 - 1 = n
<VAR>n : Nat<GOAL>1 + n - 1 = n
<VAR>n m : Nat<VAR>h : m ≤ n<GOAL>n - (n - m) = m
<VAR>n m k : Nat<VAR>h : k ≤ n<GOAL>n + m - k = n - k + m
<VAR>n m : Nat<GOAL>n - m = 0 ↔ n ≤ m
<VAR>n m : Nat<GOAL>0 < n - m ↔ m < n
<VAR>a b c : Nat<GOAL>a - b ≤ c ↔ a ≤ c + b
<VAR>a b c : Nat<GOAL>a - b ≤ c ↔ a ≤ b + c
<VAR>k m n : Nat<VAR>h : k ≤ m<GOAL>n ≤ m - k ↔ n + k ≤ m
<VAR>m k : Nat<VAR>n : Nat<VAR>h : m ≤ k<GOAL>n + m ≤ k ↔ n ≤ k - m
<VAR>n k m : Nat<VAR>h : m ≤ k<GOAL>n ≤ k - m → m + n ≤ k
<VAR>n k m : Nat<GOAL>m + n ≤ k → n ≤ k - m
<VAR>k m n : Nat<VAR>h : k ≤ m<GOAL>n ≤ m - k ↔ k + n ≤ m
<VAR>n k m : Nat<GOAL>n ≤ k → k - m ≤ k - n → n ≤ m
<VAR>n m k : Nat<VAR>h : n ≤ k<GOAL>k - m ≤ k - n ↔ n ≤ m
<VAR>a b : Nat<VAR>h₀ : 0 < a<VAR>h₁ : a ≤ b<GOAL>b - a < b
<VAR>a b c : Nat<GOAL>b < c - a → a + b < c
<VAR>m k n : Nat<VAR>h₁ : m + k ≤ n<VAR>h₂ : 0 < k<GOAL>n - (m + k) < n - m
<VAR>a b : Nat<VAR>h₀ : 0 < a<VAR>h₁ : a ≤ b<GOAL>a - 1 < b
<VAR>a b : Nat<GOAL>a - b < a.succ
<VAR>a b : Nat<GOAL>a - b < a + 1
<VAR>i n : Nat<VAR>h : i < n<GOAL>n - 1 - i < n
<VAR>m n : Nat<VAR>h : m ≤ n<GOAL>∃ k, n = m + k
<VAR>m n : Nat<VAR>h : m ≤ n<GOAL>∃ k, n = k + m
<VAR>m n : Nat<VAR>h : m < n<GOAL>∃ k, n = m + k + 1
<VAR>x y : Nat<GOAL>min x.succ y.succ = (min x y).succ
<VAR>a b c : Nat<GOAL>min (min a b) c = min a (min b c)
<VAR>m n : Nat<GOAL>min m (min m n) = min m n
<VAR>m n : Nat<GOAL>min n (min m n) = min n m
<VAR>a b : Nat<GOAL>a - (a - b) = min a b
<VAR>n m : Nat<GOAL>n - m = n - min n m
<VAR>n m : Nat<GOAL>n - m + min n m = n
<VAR>a b : Nat<VAR>h : a ≤ b<GOAL>max a b = b
<VAR>a b : Nat<VAR>h : b ≤ a<GOAL>max a b = a
<VAR>x y : Nat<GOAL>max x.succ y.succ = (max x y).succ
<VAR>a b c : Nat<GOAL>a ≤ c → b ≤ c → max a b ≤ c
<VAR>a b c : Nat<GOAL>max a b ≤ c ↔ a ≤ c ∧ b ≤ c
<VAR>a b c : Nat<GOAL>max a b < c ↔ a < c ∧ b < c
<VAR>a b c : Nat<GOAL>max (max a b) c = max a (max b c)
<VAR>a b : Nat<GOAL>a - b + b = max a b
<VAR>n m : Nat<GOAL>n - m = max n m - m
<VAR>a b c : Nat<GOAL>max a (min b c) = min (max a b) (max a c)
<VAR>a b c : Nat<GOAL>min a (max b c) = max (min a b) (min a c)
<VAR>a b c : Nat<GOAL>max (min a b) c = min (max a c) (max b c)
<VAR>a b c : Nat<GOAL>min (max a b) c = max (min a c) (min b c)
<VAR>a b c : Nat<GOAL>max (a + c) (b + c) = max a b + c
<VAR>a b c : Nat<GOAL>min (a + c) (b + c) = min a b + c
<VAR>a b c : Nat<GOAL>max (a + b) (a + c) = a + max b c
<VAR>a b c : Nat<GOAL>min (a + b) (a + c) = a + min b c
<VAR>x y : Nat<GOAL>min x.pred y.pred = (min x y).pred
<VAR>x y : Nat<GOAL>max x.pred y.pred = (max x y).pred
<VAR>a b c : Nat<GOAL>min (a - c) (b - c) = min a b - c
<VAR>a b c : Nat<GOAL>max (a - c) (b - c) = max a b - c
<VAR>a b c : Nat<GOAL>min (a - b) (a - c) = a - max b c
<VAR>a b c : Nat<GOAL>max (a - b) (a - c) = a - min b c
<VAR>a b c : Nat<GOAL>max (a * c) (b * c) = max a b * c
<VAR>a b c : Nat<GOAL>min (a * c) (b * c) = min a b * c
<VAR>a b c : Nat<GOAL>max (a * b) (a * c) = a * max b c
<VAR>a b c : Nat<GOAL>min (a * b) (a * c) = a * min b c
<VAR>a b c : Nat<GOAL>a ≤ b → c * a ≤ c * b
<VAR>a b c : Nat<GOAL>a ≤ b → a * c ≤ b * c
<VAR>n m k : Nat<GOAL>n * m * k = n * k * m
<VAR>a b c d : Nat<GOAL>a * b * (c * d) = a * c * (b * d)
<VAR>m n : Nat<GOAL>n * m = 0 ↔ n = 0 ∨ m = 0
<VAR>n m : Nat<GOAL>n * m ≠ 0 ↔ n ≠ 0 ∧ m ≠ 0
<VAR>n m : Nat<GOAL>n ≠ 0 → m ≠ 0 → n * m ≠ 0
<VAR>n m : Nat<VAR>h : n * m ≠ 0<GOAL>n ≠ 0
<VAR>n m k : Nat<VAR>np : 0 < n<VAR>h : n * m = n * k<GOAL>m = k