induction as <;> dsimp [reverseAux] <;> intro a 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)
case nil
α : Type u
r : α → α → Prop
a : α
bs : List α
⊢ Ascending (flip r) [a] → Ascending r (a :: bs) → Ascending r (a :: bs)

case cons
α : Type u
r : α → α → Prop
head✝ : α
tail✝ : List α
tail_ih✝ :
  ∀ {a : α} {bs : List α},
    Ascending (flip r) (a :: tail✝) → Ascending r (a :: bs) → Ascending r (reverseAux (a :: tail✝) bs)
a : α
bs : List α
⊢ Ascending (flip r) (a :: head✝ :: tail✝) → Ascending r (a :: bs) → Ascending r (reverseAux tail✝ (head✝ :: a :: bs))