conv => rhs; rw [and_assoc]; rhs; rw [and_comm]
case refine_1.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 ∧ ↑(x * y)[↑t.fst] > ↑(x * y)[↑t.snd]) ∧ ↑y[↑t.fst] < ↑y[↑t.snd]
no goals