proposition: Lemma is_empty_spec m : is_empty m = true <-> forall x, find x m = None.
proof: Proof. destruct m as [|h r x e l]; simpl; split; try easy. intros H. specialize (H x). now rewrite F.compare_refl in H. Qed.
imports: Coq(Bool Arith BinInt FunInd) Coq(Orders OrdersFacts OrdersLists) MMaps(Comparisons Interface OrdList)