proposition: Lemma rmax_8 : ~ occ q (Z_bnode n t1 t').
proof: Proof. intro F;case (occ_inv F). + intro eg; absurd (n < q). * rewrite eg; apply Z.lt_irrefl. * auto with searchtrees. + intro H1; case H1; intro H2. * absurd (occ q t1); auto with searchtrees. apply not_left with n (Z_bnode p t2 t3); auto with searchtrees. apply Z.le_ge; elim R1; auto with searchtrees. * elim R1; auto. Qed.
imports: ZArith Extraction List