English
For any ts and is, the length of permutationsAux ts is plus the factorial of is.length equals the factorial of the sum of their lengths: length (permutationsAux ts is) + is.length! = (length ts + length is)!.
Русский
Для любых ts и is длина permutationsAux ts is плюс факториал длины is равняется факториалу суммы длин: length (permutationsAux ts is) + is.length! = (length ts + length is)!.
LaTeX
$$$$\operatorname{length}(\mathrm{permutationsAux}\ ts\ is) + is.length! = (length\ ts + length\ is)!$$$$
Lean4
theorem length_permutationsAux :
∀ ts is : List α, length (permutationsAux ts is) + is.length ! = (length ts + length is)! :=
by
refine permutationsAux.rec (by simp) ?_
intro t ts is IH1 IH2
have IH2 : length (permutationsAux is nil) + 1 = is.length ! := by simpa using IH2
simp only [length, factorial, Nat.mul_comm, add_eq] at IH1
rw [permutationsAux_cons, length_foldr_permutationsAux2' _ _ _ _ _ fun l m => (perm_of_mem_permutations m).length_eq,
permutations, length, length, IH2, Nat.succ_add, Nat.factorial_succ, Nat.mul_comm (_ + 1), ← Nat.succ_eq_add_one, ←
IH1, Nat.add_comm (_ * _), Nat.add_assoc, Nat.mul_succ, Nat.mul_comm]
