case fst_lt_snd =>
  constructor
  case left => exact hhook.snd_Ascending.forAll_of_tail
  case right => exact hlt.right
α : 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
⊢ List.forAllRel r (b :: as) bs
no goals