Commit 2022-10-04 05:52 561202d0

refactor(data/list/count): review API, add lemmas (#16736)

• add list.countp_join, list.countp_map, list.countp_mono_left, list.countp_congr, and list.count_join;
• add @[simp] attrs to list.countp_eq_zero, list.countp_eq_length, list.count_eq_zero, and list.count_eq_length;
• golf the proofs of list.count_bind, list.count_map_of_injective, and list.count_le_count_map.