simp only [Nat.not_lt_eq, Nat.le_iff_lt_or_eq]
case refine_2.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
ht : ↑t.fst < ↑t.snd
⊢ ↑y[↑t.fst] > ↑y[↑t.snd] ↔ ¬↑y[↑t.fst] < ↑y[↑t.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)
t : Fin n × Fin n
ht : ↑t.fst < ↑t.snd
⊢ ↑y[↑t.fst] > ↑y[↑t.snd] ↔ ↑y[↑t.snd] < ↑y[↑t.fst] ∨ ↑y[↑t.snd] = ↑y[↑t.fst]