proposition: Lemma rm_6 : search_tree (Z_bnode q t0 t').
proof: Proof. right. - elim R; auto with searchtrees. - apply search_tree_r with n (Z_bnode p t1 t2); auto with searchtrees. - elim R; intros H H0 H1 H2 H3 H4; apply maj_intro; intros q0 H5. elim (Zle_lt_or_eq _ _ (H0 q0 (H1 q0 H5))); auto. + intro eg; absurd (occ q0 t0);auto. rewrite eg; auto with searchtrees. - apply min_intro; intros q0 H; apply Z.lt_trans with n. + elim R; auto with searchtrees. + elim (min_r (n:=n) (t1:=(Z_bnode p t1 t2)) (t2:=t')); auto with searchtrees. Qed.
imports: ZArith Extraction List