proposition: Lemma rm_3 : ~ occ n (Z_bnode q t0 t').
proof: Proof. intro H; case (occ_inv H). - intro eg; absurd (q < q); auto with searchtrees. apply Z.lt_irrefl. pattern q at 2; rewrite eg; auto with searchtrees. - intro D; elim D; intro H'. + elim R; intros H0 H1 H2 H3 H4 H5. absurd (occ n (Z_bnode p t1 t2)); auto with searchtrees. apply not_left with n t'; auto with searchtrees. apply Z.le_ge; auto with zarith. + absurd (occ n t'); auto with searchtrees. apply not_right with n (Z_bnode p t1 t2); auto with searchtrees. auto with zarith. Qed.
imports: ZArith Extraction List