proposition: Lemma avgnr_add n m (f : 'I_n -> E) (d : {fdist 'I_n}) (g : 'I_m -> E) (e : {fdist 'I_m}) : <|>_d f + <|>_e g = <|>_(fdistmap (@unsplit_prod n m) (d `x e)) (fun i => let (i, j) := split_prod i in f i + g j).
proof: Proof. rewrite -[<|>_e g]scale1r !avgnrE !/avgnr big_prod_ord. rewrite -(FDist.f1 d) scaler_suml -big_split; apply congr_big=>// i _. transitivity (d i *: (1%coqR *: f i + \sum_(i0 < m) e i0 *: g i0)). by rewrite scale1r scalerDr. rewrite R1E -(FDist.f1 e) scaler_suml -big_split scaler_sumr; apply congr_big=>// j _. rewrite scalerDr -!scalerDr scalerA unsplit_prodK; congr (_ *: _). rewrite fdistmapE (big_pred1 (i, j)) /= ?fdist_prodE//. move=>[i' j'] /=; rewrite xpair_eqE inE /=. apply/eqP/andP => /=; last by case => /eqP -> /eqP ->. move=>/(congr1 (@split_prod n m))/=. by rewrite (unsplit_prodK (i, j)) (unsplit_prodK (i', j')) => -[-> ->]. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg fingroup perm matrix) mathcomp(mathcomp_extra boolp classical_sets Rstruct) mathcomp(ssrnum ereal) mathcomp(lra Rstruct reals) Reals ssrR Reals_ext Ranalysis_ext ssr_ext ssralg_ext logb realType_ext fdist