proposition: Lemma rm_right : forall (n p:Z) (t1 t2 t':Z_btree), n < p -> search_tree (Z_bnode n t1 t2) -> RM p t2 t' -> RM p (Z_bnode n t1 t2) (Z_bnode n t1 t').
proof: Proof. intros n p t1 t2 t' H H0 H1; apply rm_intro. - intro H2; elim (occ_inv H2). + intro eg; apply Z.lt_irrefl with p; auto with searchtrees. pattern p at 1; rewrite <- eg; auto with searchtrees. + intro D; elim D; intro H3; elim H1; auto with searchtrees. absurd (occ p t1); auto with searchtrees. apply not_left with n t2; auto with searchtrees. apply Z.le_ge; apply Zlt_le_weak; auto. - intros p0 H2; elim (occ_inv H2). + intro e ; elim e; auto with searchtrees. + intro d ; elim d; auto with searchtrees. intro; elim H1; auto with searchtrees. - intros p0 H2; elim (occ_inv H2). + intro e ; elim e; auto with searchtrees. + intro d ; elim d; intro H4. elim H1; intros H5 H6 H7 H8. left. auto with searchtrees. elim H1; intros H5 H6 H7 H8. elim (H7 p0 H4); auto with searchtrees. - right. eauto with searchtrees. elim H1; auto. + eauto with searchtrees. + eapply min_r with t1; elim H1; intros H2 H3 H4 H5. inversion_clear H0. right; auto. * elim H9;split; intros. apply H0. elim H1; auto with searchtrees. Qed.
imports: ZArith Extraction List