proposition: Lemma elements_split : forall x s, elements s = elements_lt x s ++ elements_ge x s.
proof: Proof. unfold elements_lt, elements_ge, leb; intros. eapply (@filter_split _ E.eq _ E.lt). 1-2: auto with typeclass_instances. 2: auto with set. intros. rewrite gtb_1 in H. assert (~E.lt y x). { unfold gtb in *; destruct (E.compare x y); intuition try discriminate; ME.order. } ME.order. Qed.
imports: FSetInterface PeanoNat DecidableTypeEx FSetFacts FSetDecide