English
Let as and bs be lists with as a sublist of bs, and bs sorted with respect to r. Then inserting x into as yields a list that is a sublist of inserting x into bs: orderedInsert r x as <+ orderedInsert r x bs.
Русский
Пусть as и bs — списки, где as является подпоследовательностью bs, и bs упорядочено по r. Тогда вставка x в as дает список, который является подпоследовательностью к вставке x в bs: orderedInsert r x as <+ orderedInsert r x bs.
LaTeX
$$$ as <+ bs \\ \\wedge\\ bs.Sorted r \\Rightarrow orderedInsert r x as <+ orderedInsert r x bs $$$
Lean4
theorem orderedInsert (a : α) : ∀ l, Sorted r l → Sorted r (orderedInsert r a l)
| [], _ => sorted_singleton a
| b :: l, h => by
by_cases h' : a ≼ b
· simpa [orderedInsert, h', h] using fun b' bm => _root_.trans h' (rel_of_sorted_cons h _ bm)
· suffices ∀ b' : α, b' ∈ List.orderedInsert r a l → r b b' by
simpa [orderedInsert, h', h.of_cons.orderedInsert a l]
intro b' bm
rcases (mem_orderedInsert r).mp bm with be | bm
· subst b'
exact (total_of r _ _).resolve_left h'
· exact rel_of_sorted_cons h _ bm
