proposition: Lemma not_in_find {elt} (m : t elt) x : ~In x m <-> find x m = None.
proof: Proof. rewrite in_find. split; auto. intros; destruct (find x m); trivial. now destruct H. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)