proposition: Lemma sum_fin_num (T : Type) (s : seq T) (P : pred T) (f : T -> \bar R) : \sum_(i <- s | P i) f i \is a fin_num = all [pred x | x \is a fin_num] [seq f i | i <- s & P i].
proof: Proof. by rewrite -big_all big_map big_filter; exact: (big_morph _ fin_numD). Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed