proposition: Lemma filter_length_le : forall (X : Type) (l : list X) (f : X -> bool), length (filter f l) <= length l.
proof: Proof. intros. induction l; intuition. cbn. destruct (f a) eqn:?; intuition. cbn. lia. Qed.
imports: Coq(Lia Lists.List) Equations(Equations)