proposition: Lemma rm_left : forall (n p:Z) (t1 t2 t':Z_btree), p < n -> search_tree (Z_bnode n t1 t2) -> RM p t1 t' -> RM p (Z_bnode n t1 t2) (Z_bnode n t' t2).
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 n. pattern n at 1; rewrite eg; auto. + intro D; elim D; intro H3. elim H1; auto with searchtrees. absurd (occ p t2); auto with searchtrees. apply not_right with n t1; auto with searchtrees. apply Zlt_le_weak; auto with searchtrees. - intros p0 H2; elim (occ_inv H2). + intro e; case e; auto with searchtrees. + intro d; case d; auto with searchtrees. intro; elim H1; auto with searchtrees. - intros p0 H2; elim (occ_inv H2). + intro e; case e; auto with searchtrees. + intro d; case d; intro H4. elim H1; intros H5 H6 H7 H8. elim (H7 p0 H4); auto with searchtrees. auto with searchtrees. - right. + elim H1; auto with searchtrees. + apply search_tree_r with n t1; auto with searchtrees. + apply maj_intro; intros q H2. cut (occ q t1). * intro; elim (maj_l H0); intros; auto with searchtrees. * auto with searchtrees. elim H1; auto with searchtrees. + apply min_r with t1; auto with searchtrees. Qed.
imports: ZArith Extraction List