proposition: Lemma sum_fin_numP (T : eqType) (s : seq T) (P : pred T) (f : T -> \bar R) : reflect (forall i, i \in s -> P i -> f i \is a fin_num) (\sum_(i <- s | P i) f i \is a fin_num).
proof: Proof. rewrite sum_fin_num; apply: (iffP allP) => /=. by move=> + x xs Px; apply; rewrite map_f// mem_filter Px. by move=> + _ /mapP[x /[!mem_filter]/andP[Px xs] ->]; apply. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed