simp only [get_mul]
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]
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]]