simp only [inversionNum_eq_card_inversion]
n : Nat
x y : Permutation n
⊢ inversionNum x + inversionNum y =
    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]
n : Nat
x y : Permutation n
⊢ BishopFin.card (Inversion x) + BishopFin.card (Inversion y) =
    BishopFin.card (Inversion (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]