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 (eqbP n m) as [H | H]. + intros _. rewrite H. left. reflexivity. + intros H'. right. apply IHl'. apply H'. Qed.
imports: Coq(Lia)