proposition: Lemma elements_Add : forall m m' x e, ~In x m -> Add x e m m' -> eqlistA eqke (elements m') (elements_lt (x,e) m ++ (x,e):: elements_ge (x,e) m).
proof: Proof. intros; unfold elements_lt, elements_ge. apply sort_equivlistA_eqlistA. - auto with map. - apply (@SortA_app _ eqke). + auto with typeclass_instances. + apply (@filter_sort _ eqke). 1-3: auto with typeclass_instances. auto with map. + constructor; auto with map. * apply (@filter_sort _ eqke). 1-3: auto with typeclass_instances. auto with map. * rewrite (@InfA_alt _ eqke). 2-4: auto with typeclass_instances. -- intros. rewrite filter_InA in H1 by auto with map. destruct H1. rewrite leb_1 in H2. destruct y; unfold O.ltk in *; simpl in *. rewrite <- elements_mapsto_iff in H1. assert (~E.eq x t0). ++ contradict H. exists e0; apply MapsTo_1 with t0; auto with ordered_type. ++ ME.order. -- apply (@filter_sort _ eqke). 1-3: auto with typeclass_instances. auto with map. + intros. rewrite filter_InA in H1 by auto with map. destruct H1. rewrite gtb_1 in H3. destruct y; destruct x0; unfold O.ltk in *; simpl in *. inversion_clear H2. * red in H4; simpl in *; destruct H4. ME.order. * rewrite filter_InA in H4 by auto with map. destruct H4. rewrite leb_1 in H4. unfold O.ltk in *; simpl in *; ME.order. - red; intros a; destruct a. rewrite InA_app_iff, InA_cons, 2 filter_InA, <-2 elements_mapsto_iff, leb_1, gtb_1, find_mapsto_iff, (H0 t0), <- find_mapsto_iff, add_mapsto_iff by auto with map. unfold O.eqke, O.ltk; simpl. destruct (E.compare t0 x); intuition; try fold (~E.eq x t0); auto with ordered_type. + elim H; exists e0; apply MapsTo_1 with t0; auto. + fold (~E.lt t0 x); auto with ordered_type. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface