refine and_congr_left ?_
case refine_3.h
n : Nat
x y : Permutation n
this✝ : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
swap : Fin n × Fin n → Fin n × Fin n := fun t => (t.snd, t.fst)
this : ∀ (t : Fin n × Fin n), swap (swap t) = t
t : Fin n × Fin n
⊢ ¬↑t.snd < ↑t.fst ∧ ↑y[↑t.snd] < ↑y[↑t.fst] ∧ ↑(x * y)[↑t.snd] > ↑(x * y)[↑t.fst] ↔
    ↑t.fst < ↑t.snd ∧ ↑y[↑t.fst] > ↑y[↑t.snd] ∧ ↑(x * y)[↑t.fst] < ↑(x * y)[↑t.snd]
case refine_3.h
n : Nat
x y : Permutation n
this✝ : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
swap : Fin n × Fin n → Fin n × Fin n := fun t => (t.snd, t.fst)
this : ∀ (t : Fin n × Fin n), swap (swap t) = t
t : Fin n × Fin n
⊢ ↑y[↑t.snd] < ↑y[↑t.fst] ∧ ↑(x * y)[↑t.snd] > ↑(x * y)[↑t.fst] → (¬↑t.snd < ↑t.fst ↔ ↑t.fst < ↑t.snd)