proposition: Lemma remove_neq_in_iff : forall m x y, ~ K.eq x y -> (In y (remove x m) <-> In y m).
proof: Proof. split; intros (e',H0); exists e'. - now apply remove_3 with x. - now apply remove_2. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)