proposition: Lemma min_intro : forall (z : Z) (t : Z_btree), (forall z':Z, occ z' t -> z < z') -> min z t.
proof: Proof. induction t as [ | r t1 IHt1 t2 IHt2]. - auto with searchtrees. - intro H; apply min_bnode. + apply IHt1;intros; apply H; eauto with searchtrees. + apply IHt2;intros; apply H; eauto with searchtrees. + eauto with searchtrees. Qed.
imports: ZArith