proposition: Lemma adde_def_sum I h t (P : pred I) (f : I -> \bar R) : {in P, forall i : I, f h +? f i} -> f h +? \sum_(j <- t | P j) f j.
proof: Proof. move=> fhi; elim/big_rec : _; first by rewrite fin_num_adde_defl. by move=> i x Pi fhx; rewrite adde_defDr// fhi. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed