proposition: Lemma rmax_9 : forall q0:Z, occ q0 (Z_bnode n t1 (Z_bnode p t2 t3)) -> occ q0 (Z_bnode n t1 t') \/ q = q0.
proof: Proof. intros q0 H; elim (occ_inv H). - intro e; elim e; left; auto with searchtrees. - intro d; case d; intro H'. + left; auto with searchtrees. + elim R1; intros H1 H2 H3 H4 H5 H6. elim (H4 _ H'); auto with searchtrees. Qed.
imports: ZArith Extraction List