rewrite [Inversion.card_eq x]
n : Nat
x y : Permutation n
⊢ BishopFin.card (Inversion x) = BishopFin.count fun t => ↑y[↑t.fst] < ↑y[↑t.snd] ∧ ↑(x * y)[↑t.fst] > ↑(x * y)[↑t.snd]
n : Nat
x y : Permutation n
⊢ (BishopFin.count fun t => ↑t.fst < ↑t.snd ∧ ↑x[↑t.fst] > ↑x[↑t.snd]) =
    BishopFin.count fun t => ↑y[↑t.fst] < ↑y[↑t.snd] ∧ ↑(x * y)[↑t.fst] > ↑(x * y)[↑t.snd]