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