proposition: Lemma elements_Add_Below : forall s s' x, Below x s -> Add x s s' -> eqlistA E.eq (elements s') (x::elements s).
proof: Proof. intros. apply sort_equivlistA_eqlistA; auto with set. - change (sort E.lt ((x::nil) ++ elements s)). apply (@SortA_app _ E.eq); auto with *. intros. invlist InA. rewrite <- elements_iff in H2. setoid_replace x0 with x; auto. - red; intros a. rewrite InA_cons, <- !elements_iff, (H0 a); intuition. Qed.
imports: MSetInterface PeanoNat DecidableTypeEx OrdersLists MSetFacts MSetDecide