∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerable α] {a b c : α},
  Std.PRange.UpwardEnumerable.LE a b → Std.PRange.UpwardEnumerable.LT b c → Std.PRange.UpwardEnumerable.LT a c