proposition: Lemma elements_Add : forall s s' x, ~In x s -> Add x s s' -> eqlistA E.eq (elements s') (elements_lt x s ++ x :: elements_ge x s).
proof: Proof. intros; unfold elements_ge, elements_lt. apply sort_equivlistA_eqlistA; auto with set. - apply (@SortA_app _ E.eq); auto with *. + apply (@filter_sort _ E.eq); auto with *; eauto with *. + constructor; auto. * apply (@filter_sort _ E.eq); auto with *; eauto with *. * rewrite Inf_alt by (apply (@filter_sort _ E.eq); eauto with *). intros. rewrite filter_InA in H1; auto with *; destruct H1. rewrite leb_1 in H2. rewrite <- elements_iff in H1. assert (~E.eq x y). { contradict H; rewrite H; auto. } order. + intros. rewrite filter_InA in H1; auto with *; destruct H1. rewrite gtb_1 in H3. inversion_clear H2. * order. * rewrite filter_InA in H4; auto with *; destruct H4. rewrite leb_1 in H4. order. - red; intros a. rewrite InA_app_iff, InA_cons, !filter_InA, <-!elements_iff, leb_1, gtb_1, (H0 a) by (auto with *). intuition. elim_compare a x; intuition. right; right; split; auto. order. Qed.
imports: MSetInterface PeanoNat DecidableTypeEx OrdersLists MSetFacts MSetDecide