have : ∀ (a b c d : Nat), (a + b) + (c + d) = (a + c) + (b + d) :=
  fun a b c d => by
    conv => lhs; rw [Nat.add_assoc, ← Nat.add_assoc b, Nat.add_comm b c, Nat.add_assoc c, ← Nat.add_assoc a]
n : Nat
x y : Permutation n
⊢ ((BishopFin.count fun a => (↑y[↑a.fst] < ↑y[↑a.snd] ∧ ↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd]) ∧ ↑a.fst < ↑a.snd) +
        BishopFin.count fun a => (↑y[↑a.fst] < ↑y[↑a.snd] ∧ ↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd]) ∧ ¬↑a.fst < ↑a.snd) +
      ((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 ∧ ↑y[↑a.fst] > ↑y[↑a.snd]) ∧ ¬↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd]) =
    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]
n : Nat
x y : Permutation n
this : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
⊢ ((BishopFin.count fun a => (↑y[↑a.fst] < ↑y[↑a.snd] ∧ ↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd]) ∧ ↑a.fst < ↑a.snd) +
        BishopFin.count fun a => (↑y[↑a.fst] < ↑y[↑a.snd] ∧ ↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd]) ∧ ¬↑a.fst < ↑a.snd) +
      ((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 ∧ ↑y[↑a.fst] > ↑y[↑a.snd]) ∧ ¬↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd]) =
    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]