proposition: Lemma elements_split : forall p m, elements m = elements_lt p m ++ elements_ge p m.
proof: Proof. unfold elements_lt, elements_ge, leb; intros. apply filter_split with (eqA:=eqk) (ltA:=ltk). 1-3: auto with typeclass_instances. 2: auto with map. intros; destruct x; destruct y; destruct p. rewrite gtb_1 in H; unfold O.ltk in H; simpl in *. assert (~ltk (t1,e0) (k,e1)). - unfold gtb, O.ltk in *; simpl in *. destruct (E.compare k t1); intuition; try discriminate; ME.order. - unfold O.ltk in *; simpl in *; ME.order. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface