fact: Fixpoint insert_in_searchtree (n:Z)(t: Zbtree) : Zbtree := match t with | leaf => bnode n leaf leaf | bnode r t1 t2 => match Z.compare n r with | Lt => bnode r (insert_in_searchtree n t1) t2 | Eq => t | Gt => bnode r t1 (insert_in_searchtree n t2) end end.
imports: Bool ZArith List