proposition: Lemma rmax_7 : forall q':Z, occ q' (Z_bnode n t1 t') -> occ q' (Z_bnode n t1 (Z_bnode p t2 t3)).
proof: Proof. intros q' H; elim (occ_inv H); intro H0. - elim H0; auto with searchtrees. - elim H0; auto with searchtrees. intro H1; elim R1; auto with searchtrees. Qed.
imports: ZArith Extraction List