dsimp [cyclic]
m n✝ n : Nat
i : Fin n
l : List (Fin n)
h : ¬i ∈ l
⊢ sign (cyclic (i :: l)) = (List.length l % 2 == 1)
m n✝ n : Nat
i : Fin n
l : List (Fin n)
h : ¬i ∈ l
⊢ sign (List.foldr (fun j x => swap x i j) 1 l) = (List.length l % 2 == 1)