ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>toIcoMod hp a b ∈ Set.Ico a (a + p)
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>b : α<GOAL>toIcoMod hp 0 b ∈ Set.Ico 0 p
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>toIocMod hp a b ∈ Set.Ioc a (a + p)
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>a ≤ toIcoMod hp a b
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>a < toIocMod hp a b
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>toIcoMod hp a b < a + p
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>toIocMod hp a b ≤ a + p
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>b - toIcoDiv hp a b • p = toIcoMod hp a b
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>b - toIocDiv hp a b • p = toIocMod hp a b
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>toIcoDiv hp a b • p - b = -toIcoMod hp a b
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>toIocDiv hp a b • p - b = -toIocMod hp a b
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>toIcoMod hp a b - b = -toIcoDiv hp a b • p
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>toIocMod hp a b - b = -toIocDiv hp a b • p
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>b - toIcoMod hp a b = toIcoDiv hp a b • p
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>b - toIocMod hp a b = toIocDiv hp a b • p
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>toIcoMod hp a b + toIcoDiv hp a b • p = b
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>toIocMod hp a b + toIocDiv hp a b • p = b
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>toIcoDiv hp a b • p + toIcoMod hp a b = b
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>toIocDiv hp a b • p + toIocMod hp a b = b
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b c : α<GOAL>toIcoMod hp a b = c ↔ c ∈ Set.Ico a (a + p) ∧ ∃ z, b = c + z • p
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b c : α<GOAL>toIocMod hp a b = c ↔ c ∈ Set.Ioc a (a + p) ∧ ∃ z, b = c + z • p
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a : α<GOAL>toIcoDiv hp a a = 0
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a : α<GOAL>toIocDiv hp a a = -1
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a : α<GOAL>toIcoMod hp a a = a
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a : α<GOAL>toIocMod hp a a = a + p
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a : α<GOAL>toIcoDiv hp a (a + p) = 1
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a : α<GOAL>toIocDiv hp a (a + p) = 0
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a : α<GOAL>toIcoMod hp a (a + p) = a
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a : α<GOAL>toIocMod hp a (a + p) = a + p
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<VAR>m : ℤ<GOAL>toIcoDiv hp a (b + m • p) = toIcoDiv hp a b + m
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<VAR>m : ℤ<GOAL>toIcoDiv hp (a + m • p) b = toIcoDiv hp a b - m
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<VAR>m : ℤ<GOAL>toIocDiv hp a (b + m • p) = toIocDiv hp a b + m
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<VAR>m : ℤ<GOAL>toIocDiv hp (a + m • p) b = toIocDiv hp a b - m
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<VAR>m : ℤ<GOAL>toIcoDiv hp a (m • p + b) = m + toIcoDiv hp a b
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<VAR>m : ℤ<GOAL>toIocDiv hp a (m • p + b) = m + toIocDiv hp a b
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<VAR>m : ℤ<GOAL>toIcoDiv hp a (b - m • p) = toIcoDiv hp a b - m
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<VAR>m : ℤ<GOAL>toIcoDiv hp (a - m • p) b = toIcoDiv hp a b + m
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<VAR>m : ℤ<GOAL>toIocDiv hp a (b - m • p) = toIocDiv hp a b - m
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<VAR>m : ℤ<GOAL>toIocDiv hp (a - m • p) b = toIocDiv hp a b + m
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>toIcoDiv hp a (b + p) = toIcoDiv hp a b + 1
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>toIcoDiv hp (a + p) b = toIcoDiv hp a b - 1
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>toIocDiv hp a (b + p) = toIocDiv hp a b + 1
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>toIocDiv hp (a + p) b = toIocDiv hp a b - 1
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>toIcoDiv hp a (p + b) = toIcoDiv hp a b + 1
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>toIcoDiv hp (p + a) b = toIcoDiv hp a b - 1
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>toIocDiv hp a (p + b) = toIocDiv hp a b + 1
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>toIocDiv hp (p + a) b = toIocDiv hp a b - 1
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>toIcoDiv hp a (b - p) = toIcoDiv hp a b - 1
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>toIcoDiv hp (a - p) b = toIcoDiv hp a b + 1
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>toIocDiv hp a (b - p) = toIocDiv hp a b - 1
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>toIocDiv hp (a - p) b = toIocDiv hp a b + 1
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b c : α<GOAL>toIcoDiv hp a (b - c) = toIcoDiv hp (a + c) b
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b c : α<GOAL>toIocDiv hp a (b - c) = toIocDiv hp (a + c) b
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b c : α<GOAL>toIcoDiv hp (a - c) b = toIcoDiv hp a (b + c)
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b c : α<GOAL>toIocDiv hp (a - c) b = toIocDiv hp a (b + c)
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>toIcoDiv hp a (-b) = -(toIocDiv hp (-a) b + 1)
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>toIcoDiv hp (-a) b = -(toIocDiv hp a (-b) + 1)
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>toIocDiv hp a (-b) = -(toIcoDiv hp (-a) b + 1)
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>toIocDiv hp (-a) b = -(toIcoDiv hp a (-b) + 1)
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<VAR>m : ℤ<GOAL>toIcoMod hp a (b + m • p) = toIcoMod hp a b
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<VAR>m : ℤ<GOAL>toIcoMod hp (a + m • p) b = toIcoMod hp a b + m • p
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<VAR>m : ℤ<GOAL>toIocMod hp a (b + m • p) = toIocMod hp a b
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<VAR>m : ℤ<GOAL>toIocMod hp (a + m • p) b = toIocMod hp a b + m • p
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<VAR>m : ℤ<GOAL>toIcoMod hp a (m • p + b) = toIcoMod hp a b
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<VAR>m : ℤ<GOAL>toIcoMod hp (m • p + a) b = m • p + toIcoMod hp a b
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<VAR>m : ℤ<GOAL>toIocMod hp a (m • p + b) = toIocMod hp a b
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<VAR>m : ℤ<GOAL>toIocMod hp (m • p + a) b = m • p + toIocMod hp a b
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<VAR>m : ℤ<GOAL>toIcoMod hp a (b - m • p) = toIcoMod hp a b
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<VAR>m : ℤ<GOAL>toIcoMod hp (a - m • p) b = toIcoMod hp a b - m • p
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<VAR>m : ℤ<GOAL>toIocMod hp a (b - m • p) = toIocMod hp a b
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<VAR>m : ℤ<GOAL>toIocMod hp (a - m • p) b = toIocMod hp a b - m • p
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>toIcoMod hp a (b + p) = toIcoMod hp a b
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>toIcoMod hp (a + p) b = toIcoMod hp a b + p
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>toIocMod hp a (b + p) = toIocMod hp a b
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>toIocMod hp (a + p) b = toIocMod hp a b + p
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>toIcoMod hp a (p + b) = toIcoMod hp a b
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>toIcoMod hp (p + a) b = p + toIcoMod hp a b
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>toIocMod hp a (p + b) = toIocMod hp a b
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>toIocMod hp (p + a) b = p + toIocMod hp a b
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>toIcoMod hp a (b - p) = toIcoMod hp a b
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>toIcoMod hp (a - p) b = toIcoMod hp a b - p
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>toIocMod hp a (b - p) = toIocMod hp a b
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>toIocMod hp (a - p) b = toIocMod hp a b - p
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b c : α<GOAL>toIcoMod hp a (b - c) = toIcoMod hp (a + c) b - c
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b c : α<GOAL>toIocMod hp a (b - c) = toIocMod hp (a + c) b - c
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b c : α<GOAL>toIcoMod hp a (b + c) = toIcoMod hp (a - c) b + c
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b c : α<GOAL>toIocMod hp a (b + c) = toIocMod hp (a - c) b + c
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>toIcoMod hp a (-b) = p - toIocMod hp (-a) b
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>toIcoMod hp (-a) b = p - toIocMod hp a (-b)
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>toIocMod hp a (-b) = p - toIcoMod hp (-a) b
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>toIocMod hp (-a) b = p - toIcoMod hp a (-b)
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b c : α<GOAL>toIcoMod hp a b = toIcoMod hp a c ↔ ∃ n, c - b = n • p
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b c : α<GOAL>toIocMod hp a b = toIocMod hp a c ↔ ∃ n, c - b = n • p
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>a ≡ b [PMOD p] ↔ toIcoMod hp a b = a
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>a ≡ b [PMOD p] ↔ toIocMod hp a b = a + p
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>[a ≡ b [PMOD p], ∀ (z : ℤ), b - z • p ∉ Set.Ioo a (a + p), toIcoMod hp a b ≠ toIocMod hp a b, toIcoMod hp a b + p = toIocMod hp a b].TFAE
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>a ≡ b [PMOD p] ↔ ∀ (z : ℤ), b - z • p ∉ Set.Ioo a (a + p)
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>a ≡ b [PMOD p] ↔ toIcoMod hp a b ≠ toIocMod hp a b
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>a ≡ b [PMOD p] ↔ toIcoMod hp a b + p = toIocMod hp a b
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>¬a ≡ b [PMOD p] ↔ toIcoMod hp a b = toIocMod hp a b
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>¬a ≡ b [PMOD p] ↔ toIcoDiv hp a b = toIocDiv hp a b
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>a ≡ b [PMOD p] ↔ toIcoDiv hp a b = toIocDiv hp a b + 1
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b c : α<GOAL>toIcoMod hp c a = toIcoMod hp c b ↔ a ≡ b [PMOD p]
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a : α<GOAL>{b | toIcoMod hp a b = toIocMod hp a b} = ⋃ z, Set.Ioo (a + z • p) (a + p + z • p)
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>toIocDiv hp a b ⩿ toIcoDiv hp a b
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>toIcoMod hp a b ≤ toIocMod hp a b
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>toIocMod hp a b ≤ toIcoMod hp a b + p
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>toIcoMod hp a b = b ↔ b ∈ Set.Ico a (a + p)
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>toIocMod hp a b = b ↔ b ∈ Set.Ioc a (a + p)
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a₁ a₂ b : α<GOAL>toIcoMod hp a₁ (toIcoMod hp a₂ b) = toIcoMod hp a₁ b
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a₁ a₂ b : α<GOAL>toIcoMod hp a₁ (toIocMod hp a₂ b) = toIcoMod hp a₁ b
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a₁ a₂ b : α<GOAL>toIocMod hp a₁ (toIocMod hp a₂ b) = toIocMod hp a₁ b
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a₁ a₂ b : α<GOAL>toIocMod hp a₁ (toIcoMod hp a₂ b) = toIocMod hp a₁ b
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a : α<GOAL>Function.Periodic (toIcoMod hp a) p
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a : α<GOAL>Function.Periodic (toIocMod hp a) p
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>toIcoMod hp 0 (a - b) = p - toIocMod hp 0 (b - a)
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>toIocMod hp 0 (a - b) = p - toIcoMod hp 0 (b - a)
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>toIcoDiv hp a b = toIcoDiv hp 0 (b - a)
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>toIocDiv hp a b = toIocDiv hp 0 (b - a)
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>toIcoMod hp a b = toIcoMod hp 0 (b - a) + a
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>toIocMod hp a b = toIocMod hp 0 (b - a) + a
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>toIcoMod hp 0 (a - b) + toIocMod hp 0 (b - a) = p
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>toIocMod hp 0 (a - b) + toIcoMod hp 0 (b - a) = p
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a : α<VAR>x : ↑(Set.Ico a (a + p))<GOAL>(QuotientAddGroup.equivIcoMod hp a).symm x = ↑↑x
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>(QuotientAddGroup.equivIcoMod hp a) ↑b = ⟨toIcoMod hp a b, ⋯⟩
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a : α<GOAL>(QuotientAddGroup.equivIcoMod hp a) 0 = ⟨toIcoMod hp a 0, ⋯⟩
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a : α<VAR>x : ↑(Set.Ioc a (a + p))<GOAL>(QuotientAddGroup.equivIocMod hp a).symm x = ↑↑x
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>(QuotientAddGroup.equivIocMod hp a) ↑b = ⟨toIocMod hp a b, ⋯⟩
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a : α<GOAL>(QuotientAddGroup.equivIocMod hp a) 0 = ⟨toIocMod hp a 0, ⋯⟩
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>x₁ x₂ x₃ : α<GOAL>toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃ ↔ toIcoMod hp 0 (x₂ - x₁) + toIcoMod hp 0 (x₁ - x₃) ≤ p
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>x₁ x₂ x₃ : α<VAR>h : toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃<GOAL>toIcoMod hp x₂ x₃ ≤ toIocMod hp x₂ x₁
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b c : α<VAR>h₁₂₃ : toIcoMod hp a b ≤ toIocMod hp a c<VAR>h₁₃₂ : toIcoMod hp a c ≤ toIocMod hp a b<GOAL>b ≡ a [PMOD p] ∨ c ≡ b [PMOD p] ∨ a ≡ c [PMOD p]
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b c : α<GOAL>toIcoMod hp b a ≤ toIocMod hp b c ∨ toIcoMod hp b c ≤ toIocMod hp b a
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b c : α<GOAL>toIcoMod hp a b ≤ toIocMod hp a c ∨ toIcoMod hp c b ≤ toIocMod hp c a
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>x₁ x₂ x₃ x₄ : α<VAR>h₁₂₃ : toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃ ∧ ¬toIcoMod hp x₃ x₂ ≤ toIocMod hp x₃ x₁<VAR>h₂₃₄ : toIcoMod hp x₂ x₄ ≤ toIocMod hp x₂ x₃ ∧ ¬toIcoMod hp x₃ x₄ ≤ toIocMod hp x₃ x₂<GOAL>toIcoMod hp x₁ x₄ ≤ toIocMod hp x₁ x₃ ∧ ¬toIcoMod hp x₃ x₄ ≤ toIocMod hp x₃ x₁
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp' : Fact (0 < p)<VAR>x₁ x₂ x₃ : α<GOAL>btw ↑x₁ ↑x₂ ↑x₃ ↔ toIcoMod ⋯ 0 (x₂ - x₁) ≤ toIocMod ⋯ 0 (x₃ - x₁)
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp' : Fact (0 < p)<VAR>x₁ x₂ x₃ : α<GOAL>btw ↑x₁ ↑x₂ ↑x₃ ↔ toIcoMod ⋯ x₁ x₂ ≤ toIocMod ⋯ x₁ x₃
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>FloorRing α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>toIcoDiv hp a b = ⌊(b - a) / p⌋
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>FloorRing α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>toIocDiv hp a b = -⌊(a + p - b) / p⌋
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>FloorRing α<VAR>b : α<GOAL>toIcoDiv ⋯ 0 b = ⌊b⌋
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>FloorRing α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>toIcoMod hp a b = a + Int.fract ((b - a) / p) * p
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>FloorRing α<VAR>p : α<VAR>hp : 0 < p<VAR>b : α<GOAL>toIcoMod hp 0 b = Int.fract (b / p) * p
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>FloorRing α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>toIocMod hp a b = a + p - Int.fract ((a + p - b) / p) * p
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>FloorRing α<VAR>b : α<GOAL>toIcoMod ⋯ 0 b = Int.fract b
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a : α<GOAL>⋃ n, Set.Ioc (a + n • p) (a + (n + 1) • p) = Set.univ
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a : α<GOAL>⋃ n, Set.Ico (a + n • p) (a + (n + 1) • p) = Set.univ
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a : α<GOAL>⋃ n, Set.Icc (a + n • p) (a + (n + 1) • p) = Set.univ
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>Archimedean α<VAR>p : α<VAR>hp : 0 < p<GOAL>⋃ n, Set.Ioc (n • p) ((n + 1) • p) = Set.univ
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>Archimedean α<VAR>p : α<VAR>hp : 0 < p<GOAL>⋃ n, Set.Ico (n • p) ((n + 1) • p) = Set.univ