proposition: Lemma mem_find_b {elt}(m:t elt)(x:key) : mem x m = if find x m then true else false.
proof: Proof. apply eq_bool_alt. rewrite mem_find. destruct (find x m). - now split. - split; (discriminate || now destruct 1). Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)