∀ {α : Type u_1} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.Least? α]
  [inst_2 : Std.PRange.LawfulUpwardEnumerableLeast? α] {a : α},
  Std.PRange.UpwardEnumerable.LE Std.PRange.UpwardEnumerable.least a = True