Theorem: List.Ascending.reverse (Algdata/Data/List/Ascending.lean)

State before:
α : Type u
r : α → α → Prop
as : List α
hchain : Ascending r as
this : Ascending (flip (flip r)) as
⊢ relHead (flip r) as []
Tactic:
cases as <;> exact True.intro
State after:
no goals