∀ {α : Type u} {r : Std.Roi α} [inst : LT α] [inst_1 : Std.PRange.UpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLT α] [Std.Rxi.IsAlwaysFinite α] [Std.PRange.LawfulUpwardEnumerable α] {a b : α},
  Std.PRange.UpwardEnumerable.LE r.lower b → a ∈ b<...* → a ∈ r