proposition: Lemma rmax_4 : search_tree (Z_bnode n t1 t').
proof: Proof. right. - apply search_tree_l with n (Z_bnode p t2 t3); auto with searchtrees. - elim R1; auto with searchtrees. - apply maj_l with (Z_bnode p t2 t3); auto with searchtrees. - auto with searchtrees. Qed.
imports: ZArith Extraction List