apply BishopFin.count_congr
case refine_2
n : Nat
x y : Permutation n
this : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
⊢ (BishopFin.count fun a => (↑a.fst < ↑a.snd ∧ ↑y[↑a.fst] > ↑y[↑a.snd]) ∧ ↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd]) =
    BishopFin.count fun a => (↑a.fst < ↑a.snd ∧ ↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd]) ∧ ¬↑y[↑a.fst] < ↑y[↑a.snd]
case refine_2.h
n : Nat
x y : Permutation n
this : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
⊢ ∀ (a : Fin n × Fin n),
    (↑a.fst < ↑a.snd ∧ ↑y[↑a.fst] > ↑y[↑a.snd]) ∧ ↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd] ↔
      (↑a.fst < ↑a.snd ∧ ↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd]) ∧ ¬↑y[↑a.fst] < ↑y[↑a.snd]