proposition: Theorem filter_not_empty_In : forall n l, filter (fun x => n =? x) l <> [] -> In n l.
proof: Proof. intros n l. induction l as [|m l' IHl']. - simpl. intros H. apply H. reflexivity. - simpl. destruct (n =? m) eqn:H. + intros _. rewrite eqb_eq in H. rewrite H. left. reflexivity. + intros H'. right. apply IHl'. apply H'. Qed.
imports: Coq(Lia)