English
An explicit decomposition of orderedInsert using takeWhile and dropWhile: for any a and list l, l.orderedInsert r a equals takeWhile(¬ a ≼ ·) l ++ a :: dropWhile(¬ a ≼ ·) l.
Русский
Явное разложение orderedInsert через takeWhile и dropWhile: для любого a и списка l, l.orderedInsert r a = takeWhile(¬ a ≼ ·) l ++ a :: dropWhile(¬ a ≼ ·) l.
LaTeX
$$$$ \forall (a:\alpha),\forall L:\mathrm{List}(\alpha),\; L.\operatorname{orderedInsert}(r,a) = \big( L.takeWhile(\lambda b. \neg (a \preceq b)) \big) \\; ++ \\ a :: \big( L.dropWhile(\lambda b. \neg (a \preceq b)) \big). $$$$
Lean4
/-- An alternative definition of `orderedInsert` using `takeWhile` and `dropWhile`. -/
theorem orderedInsert_eq_take_drop (a : α) :
∀ l : List α, l.orderedInsert r a = (l.takeWhile fun b => ¬a ≼ b) ++ a :: l.dropWhile fun b => ¬a ≼ b
| [] => rfl
| b :: l => by
dsimp only [orderedInsert]
split_ifs with h <;> simp [takeWhile, dropWhile, *, orderedInsert_eq_take_drop a l]
