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