no goals
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
p : α
hp : 0 < p
a : α
⊢ (⋃ (n : ℤ), Icc (a + n • p) (a + (n + 1) • p)) = univ
simpa only [iUnion_Ioc_add_zsmul hp a, univ_subset_iff] using
  iUnion_mono fun n : ℤ => (Ioc_subset_Icc_self : Ioc (a + n • p) (a + (n + 1) • p) ⊆ Icc _ _)