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