proposition: Lemma remove_3bis m x y e : find y (remove x m) = Some e -> find y m = Some e.
proof: Proof. destruct (K.eq_dec x y) as [<-|H]. - now rewrite remove_spec1. - now rewrite remove_spec2. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)