apply and_congr_right
case refine_4.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
⊢ (↑t.fst < ↑t.snd ∧ ↑y[↑t.fst] > ↑y[↑t.snd]) ∧ ¬↑(x * y)[↑t.fst] > ↑(x * y)[↑t.snd] ↔
    (↑t.fst < ↑t.snd ∧ ↑y[↑t.fst] > ↑y[↑t.snd]) ∧ ↑(x * y)[↑t.fst] < ↑(x * y)[↑t.snd]
case refine_4.h.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
⊢ ↑t.fst < ↑t.snd ∧ ↑y[↑t.fst] > ↑y[↑t.snd] →
    (¬↑(x * y)[↑t.fst] > ↑(x * y)[↑t.snd] ↔ ↑(x * y)[↑t.fst] < ↑(x * y)[↑t.snd])