proposition: Lemma insert_l : forall (n p:Z) (t1 t'1 t2:Z_btree), n < p -> search_tree (Z_bnode p t1 t2) -> INSERT n t1 t'1 -> INSERT n (Z_bnode p t1 t2) (Z_bnode p t'1 t2).
proof: Proof. intros n p t1 t'1 t2 H H0 H1; split. - intros p0 H2; inversion_clear H2; auto with searchtrees. elim H1; auto with searchtrees. - constructor 2; elim H1; auto with searchtrees. - intros p0 H2; inversion_clear H2; auto with searchtrees. elim H1. intros H4 H5 H6. elim (H6 p0); auto with searchtrees. - elim H1; constructor 2; auto with searchtrees. + eapply search_tree_r; eauto with searchtrees. + split; intros; elim (H4 z'). intro; cut (maj p t1). * induction 1; auto with searchtrees. * eapply maj_l; eauto with searchtrees. * intro e; subst z'; auto with searchtrees. * assumption. + eapply min_r; eauto with searchtrees. Qed.
imports: ZArith Extraction