rewrite [BishopFin.count_eq_card]
n : Nat
x : Permutation n
⊢ BishopFin.card (Inversion x) = BishopFin.count fun t => ↑t.fst < ↑t.snd ∧ ↑x[↑t.fst] > ↑x[↑t.snd]
n : Nat
x : Permutation n
⊢ BishopFin.card (Inversion x) = BishopFin.card { a // ↑a.fst < ↑a.snd ∧ ↑x[↑a.fst] > ↑x[↑a.snd] }