exact List.Ascending.cons_of_forAll hlt.left hhook.fst_revAscending
α : Type u_1
r : α → α → Prop
inst✝ : Trans r r r
as : List α
b : α
bs : List α
hhook : HookedAscending r as (b :: bs)
hlt : forAll (fun x => r x b) as ∧ List.forAllRel r as bs
⊢ Ascending (flip r) (b :: as)
no goals