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