Theorem fin.card_filter_univ_succ'

feat(big_operators/fin): sum over elements of vector equal to `a` equals count `a` (#15360) …