proposition: Lemma insert_r : forall (n p:Z) (t1 t2 t'2: Z_btree), n > p -> search_tree (Z_bnode p t1 t2) -> INSERT n t2 t'2 -> INSERT n (Z_bnode p t1 t2) (Z_bnode p t1 t'2).
proof: Proof. intros n p t1 t2 t'2 H H0 H1; split. - intros p0 H2; inversion_clear H2; auto with searchtrees. elim H1; auto with searchtrees. - constructor 3; 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_l; eauto with searchtrees. + split; intros; elim (maj_l H0); auto with searchtrees. + split; intros q H6; elim (H4 q H6). intro; elim (min_r H0); auto with searchtrees. intro e; subst q; auto with searchtrees. apply Z.gt_lt. assumption. Qed.
imports: ZArith Extraction