∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] {bound : α} {l : List ((a : α) × β a)}
  {l_ordered : List.Pairwise (fun a b => compare a.fst b.fst = Ordering.lt) l},
  List.takeWhile (fun e => (compare e.fst bound).isLE) l = List.filter (fun e => (compare e.fst bound).isLE) l