α : Type u_1
β : Type ?u.3194
γ : Type ?u.3197
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
⊢ length (permsOfList (a :: l)) = (length l + 1) * (length l)!
α : Type u_1
β : Type ?u.3194
γ : Type ?u.3197
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
⊢ length (permsOfList (a :: l)) = (length (a :: l))!
rw [length_cons, Nat.factorial_succ]
α : Type u_1
β : Type ?u.3194
γ : Type ?u.3197
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
⊢ (length l)! + length l * (length l)! = length l * (length l)! + (length l)!
α : Type u_1
β : Type ?u.3194
γ : Type ?u.3197
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
⊢ length (permsOfList (a :: l)) = (length l + 1) * (length l)!
simp only [permsOfList, length_append, length_permsOfList, length_bind, comp,
 length_map, map_const', sum_replicate, smul_eq_mul, succ_mul]
no goals
α : Type u_1
β : Type ?u.3194
γ : Type ?u.3197
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
⊢ (length l)! + length l * (length l)! = length l * (length l)! + (length l)!
ring