revert a bs
α : Type u
r : α → α → Prop
a : α
as bs : List α
⊢ Ascending (flip r) (a :: as) → Ascending r (a :: bs) → Ascending r (reverseAux (a :: as) bs)
α : Type u
r : α → α → Prop
as : List α
⊢ ∀ {a : α} {bs : List α}, Ascending (flip r) (a :: as) → Ascending r (a :: bs) → Ascending r (reverseAux (a :: as) bs)