exact Nat.lt_irrefl _ (this ▸ ht.1)
case refine_4.h.h.hb
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]
hxyt : ↑(x * y)[↑t.fst] = ↑(x * y)[↑t.snd]
this : ↑t.fst = ↑t.snd
⊢ False
no goals