apply Ascending.reverseAux_cons
α : Type u_1
r : α → α → Prop
bs : List α
a : α
as : List α
hhook : HookedAscending r (a :: as) bs
⊢ Ascending r (reverseAux as (a :: bs))
case a
α : Type u_1
r : α → α → Prop
bs : List α
a : α
as : List α
hhook : HookedAscending r (a :: as) bs
⊢ Ascending (flip r) (a :: as)

case a
α : Type u_1
r : α → α → Prop
bs : List α
a : α
as : List α
hhook : HookedAscending r (a :: as) bs
⊢ Ascending r (a :: bs)