assumption
case a.«_@».Project.Main._hyg.2095.inr.mk.ha
α : Type u
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
a b : BinTree α
hb : IsSearchTree le b
h✝ : ¬le b.val a.val = true
a✝ : IsMinTree le a.val (nodes a.children)
⊢ IsSearchTree le b

case a.«_@».Project.Main._hyg.2095.inr.mk.hba
α : Type u
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
a b : BinTree α
hb : IsSearchTree le b
h✝ : ¬le b.val a.val = true
a✝ : IsMinTree le a.val (nodes a.children)
⊢ le a.val b.val = true
case a.«_@».Project.Main._hyg.2095.inr.mk.hba
α : Type u
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
a b : BinTree α
hb : IsSearchTree le b
h✝ : ¬le b.val a.val = true
a✝ : IsMinTree le a.val (nodes a.children)
⊢ le a.val b.val = true