proposition: Lemma rmax_t_Z_leaf : forall (t:Z_btree) (n:Z), search_tree (Z_bnode n t Z_leaf) -> RMAX (Z_bnode n t Z_leaf) t n.
proof: Proof. intros t n H; split; auto with searchtrees. - intros p H0; elim (occ_inv H0); intro H1. + subst p; auto with zarith. + elim H1; intro H2. * apply Zlt_le_weak; elim (maj_l H); auto. * absurd (occ p Z_leaf); auto with searchtrees. - intros q H1; elim (occ_inv H1); intros H0; auto with searchtrees. destruct H0; auto. inversion H0. - intro H'; absurd (occ n Z_leaf). + auto with searchtrees. + destruct (not_left H (p:=n)). * auto with zarith. * auto with searchtrees. - eauto with searchtrees. Qed.
imports: ZArith Extraction List