proposition: Lemma find_none l : find l = None -> forall x, In x l -> f x = false.
proof: Proof. induction l as [|a l IH]; simpl; [easy|]. case_eq (f a); intros Ha Eq x IN; [easy|]. destruct IN as [<-|IN]; auto. Qed.
imports: PeanoNat