conv at this =>
  dsimp; rw [Nat.add_mul_mod_self_left, Nat.add_mod]
m n : Nat
x y : Permutation n
this :
  (fun x => x % 2) (inversionNum x + inversionNum y) =
    (fun x => x % 2)
      (inversionNum (x * y) +
        2 * BishopFin.count fun t => ↑t.fst < ↑t.snd ∧ ↑y[↑t.fst] > ↑y[↑t.snd] ∧ ↑(x * y)[↑t.fst] < ↑(x * y)[↑t.snd])
⊢ sign (x * y) = (sign x != sign y)
m n : Nat
x y : Permutation n
this : (inversionNum x % 2 + inversionNum y % 2) % 2 = inversionNum (x * y) % 2
⊢ sign (x * y) = (sign x != sign y)