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 typeclass_instances. } + apply (@filter_sort _ E.eq). 1-3: auto with typeclass_instances. auto with set. + constructor; auto. * apply (@filter_sort _ E.eq). 1-3: auto with typeclass_instances. auto with set. * rewrite ME.Inf_alt by (apply (@filter_sort _ E.eq); auto with set typeclass_instances). intros. rewrite filter_InA in H1 by auto with fset. destruct H1. rewrite leb_1 in H2. rewrite <- elements_iff in H1. assert (~E.eq x y). { contradict H; rewrite H; auto. } ME.order. + intros. rewrite filter_InA in H1 by auto with fset. destruct H1. rewrite gtb_1 in H3. inversion_clear H2. * ME.order. * rewrite filter_InA in H4 by auto with fset. destruct H4. rewrite leb_1 in H4. ME.order. - red; intros a. rewrite InA_app_iff, InA_cons, !filter_InA, <-elements_iff, leb_1, gtb_1, (H0 a) by auto with fset. intuition auto with relations set. destruct (E.compare a x); intuition auto with set. fold (~E.lt a x); auto with ordered_type set. Qed.
imports: FSetInterface PeanoNat DecidableTypeEx FSetFacts FSetDecide