constructor
α : Type u_1
r r₁ : α → α → Prop
himp : ∀ (a b : α), r a b → r₁ a b
as bs : List α
hhook : HookedAscending r as bs
⊢ HookedAscending r₁ as bs
case fst_lt_snd
α : Type u_1
r r₁ : α → α → Prop
himp : ∀ (a b : α), r a b → r₁ a b
as bs : List α
hhook : HookedAscending r as bs
⊢ List.forAllRel r₁ as bs

case fst_revAscending
α : Type u_1
r r₁ : α → α → Prop
himp : ∀ (a b : α), r a b → r₁ a b
as bs : List α
hhook : HookedAscending r as bs
⊢ Ascending (flip r₁) as

case snd_Ascending
α : Type u_1
r r₁ : α → α → Prop
himp : ∀ (a b : α), r a b → r₁ a b
as bs : List α
hhook : HookedAscending r as bs
⊢ Ascending r₁ bs