English
For any L, a, b, the number of occurrences of a in L.orderedInsert r b L equals the number of occurrences of a in L plus 1 if b = a, otherwise 0.
Русский
Для любого L, a, b, количество вхождений a в L.orderedInsert(r,b,L) равно количеству вхождений a в L плюс 1, если b = a, иначе 0.
LaTeX
$$$$ \forall L:\mathrm{List}(\alpha),\forall a,b:\alpha,\; \mathrm{count}(a,\mathrm{orderedInsert}(r,b,L)) = \mathrm{count}(a,L) + \begin{cases}1,& b=a\\ 0,& b\neq a\end{cases}. $$$$
Lean4
theorem orderedInsert_count [DecidableEq α] (L : List α) (a b : α) :
count a (L.orderedInsert r b) = count a L + if b = a then 1 else 0 :=
by
rw [(L.perm_orderedInsert r b).count_eq, count_cons]
simp
