no goals
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
n : ℤ
⊢ ¬a ≡ b [PMOD p] ↔ toIcoDiv hp a b = toIocDiv hp a b
rw [not_modEq_iff_toIcoMod_eq_toIocMod hp, toIcoMod, toIocMod, sub_right_inj,
  (zsmul_strictMono_left hp).injective.eq_iff]