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); eauto with *. intros. rewrite gtb_1 in H. assert (~E.lt y x). { unfold gtb in *; elim_compare x y; intuition; try discriminate; order. } order. Qed.
imports: MSetInterface PeanoNat DecidableTypeEx OrdersLists MSetFacts MSetDecide