Commit 2021-12-31 14:15 b142b697

feat(data/list/count): add lemma count_le_count_map (#11148) Generalises count_map_map: for any f : α → β (not necessarily injective), count x l ≤ count (f x) (map f l)