English
The length of xs.sym n equals the multichoose of the length of xs by n: |xs.sym n| = multichoose(|xs|, n).
Русский
Длина xs.sym n равна multichoose(|xs|, n).
LaTeX
$$$ (xs.sym n).length = \operatorname{multichoose}(xs.length, n) $$$
Lean4
theorem length_sym {n : ℕ} {xs : List α} : (xs.sym n).length = Nat.multichoose xs.length n :=
match n, xs with
| 0, _ => by rw [List.sym, Nat.multichoose]; rfl
| n + 1, [] => by simp [List.sym]
| n + 1, x :: xs => by
rw [List.sym, length_append, length_map, length_cons]
rw [@length_sym n (x :: xs), @length_sym (n + 1) xs]
rw [Nat.multichoose_succ_succ, length_cons, add_comm]
