proposition: Lemma min_ind2 : forall (z : Z) (t : Z_btree) (P:Prop), ((forall z', occ z' t -> z < z') -> P) -> min z t -> P.
proof: Proof. induction t as [ | r t1 IHt1 t2 IHt2]. - intros P H H0; apply H. inversion 1. - intros P H H0; apply H. inversion_clear 1. + eauto with searchtrees. + apply min_less with (Z_bnode r t1 t2); eauto with searchtrees. + apply min_less with (Z_bnode r t1 t2); eauto with searchtrees. Qed.
imports: ZArith