intro hh
n : ℕ
a : Fin n → ℤ
ainj : Function.Injective a
p : Equiv.Perm (Fin n)
hp : ∀ (i j : Fin n), i ≤ j → a (p i) ≤ a (p j)
i j : Fin n
hij : i < j
h0 : i ≠ j
h2 : a (p i) ≤ a (p j)
⊢ p i ≠ p j
n : ℕ
a : Fin n → ℤ
ainj : Function.Injective a
p : Equiv.Perm (Fin n)
hp : ∀ (i j : Fin n), i ≤ j → a (p i) ≤ a (p j)
i j : Fin n
hij : i < j
h0 : i ≠ j
h2 : a (p i) ≤ a (p j)
hh : p i = p j
⊢ False