proposition: Lemma elements_Add_Below : forall m m' x e, Below x m -> Add x e m m' -> eqlistA eqke (elements m') ((x,e)::elements m).
proof: Proof. intros. apply sort_equivlistA_eqlistA. - auto with map. - change (sort ltk (((x,e)::nil) ++ elements m)). apply (@SortA_app _ eqke). + auto with typeclass_instances. + auto. + auto with map. + intros. inversion_clear H1. * destruct y; destruct x0. rewrite <- elements_mapsto_iff in H2. unfold O.eqke, O.ltk in *; simpl in *; destruct H3. apply ME.eq_lt with x; auto. apply H; firstorder. * inversion H3. - red; intros a; destruct a. rewrite InA_cons, <- 2 elements_mapsto_iff, find_mapsto_iff, (H0 t0), <- find_mapsto_iff, add_mapsto_iff. unfold O.eqke; simpl. intuition auto with relations. destruct (E.eq_dec x t0) as [Heq|Hneq]; auto. exfalso. assert (In t0 m) by (exists e0; auto). generalize (H t0 H1). ME.order. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface