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 typeclass_instances. + auto. + auto with set. + intros. inversion_clear H1. * rewrite <- elements_iff in H2. apply ME.eq_lt with x; auto. * inversion H3. - red; intros a. rewrite InA_cons. do 2 rewrite <- elements_iff; rewrite (H0 a); intuition auto with relations. Qed.
imports: FSetInterface PeanoNat DecidableTypeEx FSetFacts FSetDecide