proposition: Lemma in_add m x y e : In y m -> In y (add x e m).
proof: Proof. destruct (K.eq_dec x y) as [<-|H']. - now rewrite !in_find, add_spec1. - now rewrite !in_find, add_spec2. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)