no goals
α : Type u_1
inst✝ : OrderedRing α
a : α
⊢ Pairwise (Disjoint on fun n => Ioo (a + ↑n) (a + ↑n + 1))
simpa only [zsmul_one, Int.cast_add, Int.cast_one, ← add_assoc] using
  pairwise_disjoint_Ioo_add_zsmul a (1 : α)