proposition: Lemma filter_length_lt l x : x ∈ l → ¬P x → length (filter P l) < length l.
proof: Proof. intros [k ->]%elem_of_Permutation ?; simpl. rewrite decide_False, Nat.lt_succ_r by done. apply filter_length. Qed.
imports: stdpp(options)