α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a✝ b✝ c : α
n : ℤ
a b : α
⊢ toIocDiv hp a b = toIcoDiv hp a b ∨ toIocDiv hp a b + 1 = toIcoDiv hp a b
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a✝ b✝ c : α
n : ℤ
a b : α
⊢ toIocDiv hp a b ⩿ toIcoDiv hp a b
suffices toIocDiv hp a b = toIcoDiv hp a b ∨ toIocDiv hp a b + 1 = toIcoDiv hp a b by
  rwa [wcovby_iff_eq_or_covby, ← Order.succ_eq_iff_covby]
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a✝ b✝ c : α
n : ℤ
a b : α
⊢ ¬a ≡ b [PMOD p] ∨ a ≡ b [PMOD p]
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a✝ b✝ c : α
n : ℤ
a b : α
⊢ toIocDiv hp a b = toIcoDiv hp a b ∨ toIocDiv hp a b + 1 = toIcoDiv hp a b
rw [eq_comm, ← not_modEq_iff_toIcoDiv_eq_toIocDiv, eq_comm, ←
  modEq_iff_toIcoDiv_eq_toIocDiv_add_one]
no goals
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a✝ b✝ c : α
n : ℤ
a b : α
⊢ ¬a ≡ b [PMOD p] ∨ a ≡ b [PMOD p]
exact em' _
no goals
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a✝ b✝ c : α
n : ℤ
a b : α
this : toIocDiv hp a b = toIcoDiv hp a b ∨ toIocDiv hp a b + 1 = toIcoDiv hp a b
⊢ toIocDiv hp a b ⩿ toIcoDiv hp a b
rwa [wcovby_iff_eq_or_covby, ← Order.succ_eq_iff_covby]