apply boundLeft_descend _ haxs
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys✝ : KVChain r β
a : α
b : β a
c : α
hac : r a c
ys : KVChain r fun a => β a
h_ind :
  ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
    boundLeft c (insertWithAux f xs ys hxsys a b haxs).val.fst
xs : KVChain (flip r) fun a => β a
haxs : boundLeft a xs
b₁ : β a
ha₁ys : boundLeft a ys
ha₁xs : hingeable xs (KVChain.cons a b₁ ys ha₁ys)
ha₁a haa₁ : ¬r a a
⊢ boundLeft c
    (Option.casesOn none { val := (xs, ys), property := (_ : hingeable (xs, ys).fst (xs, ys).snd) } fun bf =>
          { val := (KVChain.cons a bf xs haxs, ys),
            property := (_ : hingeable (KVChain.cons a bf xs haxs) (KVChain.cons a bf xs haxs, ys).snd) }).val.fst
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys✝ : KVChain r β
a : α
b : β a
c : α
hac : r a c
ys : KVChain r fun a => β a
h_ind :
  ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
    boundLeft c (insertWithAux f xs ys hxsys a b haxs).val.fst
xs : KVChain (flip r) fun a => β a
haxs : boundLeft a xs
b₁ : β a
ha₁ys : boundLeft a ys
ha₁xs : hingeable xs (KVChain.cons a b₁ ys ha₁ys)
ha₁a haa₁ : ¬r a a
⊢ ∀ (a' : α), flip r a a' → flip r c a'