no goals
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b c✝ : α
n : ℤ
c : α
⊢ toIcoMod hp c a = toIcoMod hp c b ↔ a ≡ b [PMOD p]
simp_rw [toIcoMod_eq_toIcoMod, modEq_iff_eq_add_zsmul, sub_eq_iff_eq_add']