proposition: Lemma go_left : forall p:Z, occ p (Z_bnode n t1 t2) -> p < n -> occ p t1.
proof: Proof. intros p H H0; elim (occ_inv H). - intro e; elim e; absurd (p < n). + rewrite e; apply Zle_not_lt; auto with zarith. + assumption. - destruct 1;auto. absurd (occ p t2). + apply not_right; apply Zlt_le_weak; assumption. + auto. Qed.
imports: ZArith Extraction