proposition: Lemma not_find_iff : forall m x, bst m -> (find x m = None <-> ~In x m).
proof: Proof. split; intros. - red; intros. elim (in_find H H1 H0). - case_eq (find x m); [ intros | auto ]. elim H0; apply find_in; congruence. Qed.
imports: FunInd FMapInterface FMapList ZArith Int