no goals
α : Type u_1
l✝ : List α
p q : α → Bool
l : List α
⊢ length (filter p l) < length l ↔ ∃ x, x ∈ l ∧ ¬p x = true
simpa [length_eq_countp_add_countp p l, countp_eq_length_filter] using
countp_pos (fun x => ¬p x) (l := l)