proposition: Lemma elements_Add_Above : forall s s' x, Above x s -> Add x s s' -> eqlistA E.eq (elements s') (elements s ++ x::nil).
proof: Proof. intros. apply sort_equivlistA_eqlistA. { auto with set. } - apply (@SortA_app _ E.eq). + auto with typeclass_instances. + auto with set. + auto. + intros. inversion_clear H2. * rewrite <- elements_iff in H1. apply ME.lt_eq with x; auto with ordered_type. * inversion H3. - red; intros a. rewrite InA_app_iff, InA_cons, InA_nil. do 2 rewrite <- elements_iff; rewrite (H0 a); intuition auto with relations. Qed.
imports: FSetInterface PeanoNat DecidableTypeEx FSetFacts FSetDecide