case intro
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a c : α
n✝ n : ℤ
⊢ toIcoMod hp a (a + n • p) = a
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
n : ℤ
⊢ (∃ z, b = a + z • p) → toIcoMod hp a b = a
rintro ⟨n, rfl⟩
no goals
case intro
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a c : α
n✝ n : ℤ
⊢ toIcoMod hp a (a + n • p) = a
rw [toIcoMod_add_zsmul, toIcoMod_apply_left]