∀ {α : Type u_1} [inst : Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerable α] (LargeEnough : α → Prop),
  (∀ (a b : α), Std.PRange.UpwardEnumerable.LE a b → LargeEnough a → LargeEnough b) →
    ∀ (next : α), LargeEnough next → ∀ (next' : α), Std.PRange.succ? next = some next' → LargeEnough next'