intro t
case refine_1.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),
    (↑y[↑a.fst] < ↑y[↑a.snd] ∧ ↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd]) ∧ ↑a.fst < ↑a.snd ↔
      (↑a.fst < ↑a.snd ∧ ↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd]) ∧ ↑y[↑a.fst] < ↑y[↑a.snd]
case refine_1.h
n : Nat
x y : Permutation n
this : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
t : Fin n × Fin n
⊢ (↑y[↑t.fst] < ↑y[↑t.snd] ∧ ↑(x * y)[↑t.fst] > ↑(x * y)[↑t.snd]) ∧ ↑t.fst < ↑t.snd ↔
    (↑t.fst < ↑t.snd ∧ ↑(x * y)[↑t.fst] > ↑(x * y)[↑t.snd]) ∧ ↑y[↑t.fst] < ↑y[↑t.snd]