Proof of fset_of_mset_count_bound