proposition: Lemma in_find {elt} (m : t elt) x : In x m <-> find x m <> None.
proof: Proof. unfold In. split. - intros (e,H). rewrite <-find_spec in H. congruence. - destruct (find x m) as [e|] eqn:H. + exists e. now apply find_spec. + now destruct 1. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)