proposition: Lemma not_find_iff m x `{!Ok m} : find x m = None <-> ~ x ∈ m.
proof: Proof. rewrite <- find_in_iff; trivial. destruct (find x m); split; try easy. now destruct 1. Qed.
imports: Coq(Bool Arith BinInt FunInd) Coq(Orders OrdersFacts OrdersLists) MMaps(Comparisons Interface OrdList)