proposition: Lemma rmax_6 : forall p0:Z, occ p0 (Z_bnode n t1 (Z_bnode p t2 t3)) -> p0 <= q.
proof: Proof. intros p0 H; elim R1; intros H0 H1 H2 H3 H4 H5. elim (occ_inv H); intro H6. - elim H6; apply Zlt_le_weak; auto with searchtrees zarith. - elim H6; intro H7; elim (maj_l S1). intro H8; cut (p0 < n); auto with searchtrees. intro; apply Zlt_le_weak; apply Z.lt_trans with n; auto with searchtrees. elim (min_r S1); auto with searchtrees. Qed.
imports: ZArith Extraction List