proposition: Lemma insert_l : forall (n p:key) (v v':data) (t1 t'1 t2:btree), Key.lt n p -> search_tree (bnode p v' t1 t2) -> INSERT n v t1 t'1 -> INSERT n v (bnode p v' t1 t2) (bnode p v' t'1 t2).
proof: Proof. intros n p v v' t1 t'1 t2 H H0 H1; split. - intros p0 v'0 H2; inversion_clear H2; auto with searchtrees. case H1; intros H2 H4 H5 H6; case (H2 _ _ H3); auto with searchtrees. - case H1; intros H2 H3 H4 H5; eauto with searchtrees. - intros p0 v'0 H2; inversion_clear H2; auto with searchtrees. case H1; intros H2 H4 H5 H6; elim (H5 p0 v'0); auto with searchtrees. - case H1; constructor 2; auto with searchtrees. eapply search_tree_r; eauto with searchtrees. split; intros k' v0 H6; elim (H4 _ _ H6). intro H7; assert (H8:maj p t1). + eauto with searchtrees. + inversion_clear H8; eauto with searchtrees. + repeat simple destruct 1; eauto with searchtrees. + eauto with searchtrees. Qed.
imports: Relations List ZArith Arith