apply Ascending.of_implies this
α : Type u_1
r : α → α → Prop
as bs : List α
hhook : HookedAscending r as bs
this : ∀ (a b : α), r a b → flip (flip r) a b
⊢ Ascending (flip (flip r)) bs
α : Type u_1
r : α → α → Prop
as bs : List α
hhook : HookedAscending r as bs
this : ∀ (a b : α), r a b → flip (flip r) a b
⊢ Ascending (fun a b => r a b) bs