proposition: Lemma filter_length {A} p (l : list A) : length (filter p l) <= length l.
proof: Proof. induction l ; simpl ; auto. destruct (p a); simpl; auto with arith. Qed.
imports: Program Utf8 Equations.Prop.Equations Bvector List Relations Arith Wf_nat Lia Coq.Lists.SetoidList Coq.Sorting.Sorting Coq.Sorting.Permutation Coq.Sorting.PermutSetoid Bool EquivDec Permutation