∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a : α) (b : α ⧸ AddSubgroup.zmultiples p), ⋯.lift b ∈ Set.Ico a (a + p)