no goals
α : Type u_1
inst✝¹ : LinearOrderedRing α
inst✝ : Archimedean α
a : α
⊢ (⋃ (n : ℤ), Icc (a + ↑n) (a + ↑n + 1)) = univ
simpa only [zsmul_one, Int.cast_add, Int.cast_one, ← add_assoc] using
  iUnion_Icc_add_zsmul zero_lt_one a