no goals
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
p : α
hp : 0 < p
a : α
⊢ (⋃ (n : ℤ), Ico (n • p) ((n + 1) • p)) = univ
simpa only [zero_add] using iUnion_Ico_add_zsmul hp 0