α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
n : ℤ
⊢ ∃ z, b = b + z • p
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
n : ℤ
⊢ toIcoMod hp a b = b ↔ b ∈ Set.Ico a (a + p)
rw [toIcoMod_eq_iff, and_iff_left]
no goals
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
n : ℤ
⊢ ∃ z, b = b + z • p
exact ⟨0, by simp⟩
no goals
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
n : ℤ
⊢ b = b + 0 • p
simp