exact hhook.fst_revAscending.of_implies this
α : Type u_1
r r₁ : α → α → Prop
himp : ∀ (a b : α), r a b → r₁ a b
as bs : List α
hhook : HookedAscending r as bs
this : ∀ (a b : α), flip r a b → flip r₁ a b
⊢ Ascending (flip r₁) as
no goals