proposition: Lemma add_id (m: t elt) x e : add x e m == m <-> find x m = Some e.
proof: Proof. split. - intros H. rewrite <- (H x). apply add_spec1. - intros H y. rewrite !add_o. now destruct K.eq_dec as [<-|E]. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)