proposition: Lemma add_in_iff m x y e : In y (add x e m) <-> K.eq x y \/ In y m.
proof: Proof. split. - intros H. destruct (K.eq_dec x y); [now left|right]. rewrite in_find, add_spec2 in H; trivial. now apply in_find. - intros [<-|H]. + exists e. now apply add_1. + now apply in_add. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)