proposition: Lemma rm_4 : forall p0:Z, occ p0 (Z_bnode q t0 t') -> occ p0 (Z_bnode n (Z_bnode p t1 t2) t').
proof: Proof. intros p0 H; case (occ_inv H). - intro eg; elim R; rewrite eg; auto with searchtrees. - intro D; elim D; auto with searchtrees. intro H'; elim R; auto with searchtrees. Qed.
imports: ZArith Extraction List