conv =>
  rhs; rewrite [beq_iff_eq, Nat.succ_eq_add_one, Nat.add_mod]
  change (l.length % 2 + 1) % 2 = 1
case cons
m n✝ n : Nat
i j : Fin n
l : List (Fin n)
IH : ¬i ∈ l → sign (List.foldr (fun j x => swap x i j) 1 l) = (List.length l % 2 == 1)
h : ¬i = j ∧ ¬i ∈ l
⊢ ¬List.length l % 2 = 1 ↔ (Nat.succ (List.length l) % 2 == 1) = true
case cons
m n✝ n : Nat
i j : Fin n
l : List (Fin n)
IH : ¬i ∈ l → sign (List.foldr (fun j x => swap x i j) 1 l) = (List.length l % 2 == 1)
h : ¬i = j ∧ ¬i ∈ l
⊢ ¬List.length l % 2 = 1 ↔ (List.length l % 2 + 1) % 2 = 1