cases Fin.eq_of_val_eq ht'
case refine_3.h.hb.mk
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), (t.fst, t.snd) = t
fst✝ snd✝ : Fin n
ht : ↑y[↑snd✝] < ↑y[↑fst✝] ∧ ↑(x * y)[↑snd✝] > ↑(x * y)[↑fst✝]
ht' : ↑fst✝ = ↑snd✝
⊢ False
case refine_3.h.hb.mk.refl
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), (t.fst, t.snd) = t
fst✝ : Fin n
ht : ↑y[↑fst✝] < ↑y[↑fst✝] ∧ ↑(x * y)[↑fst✝] > ↑(x * y)[↑fst✝]
ht' : ↑fst✝ = ↑fst✝
⊢ False