proposition: Lemma eq_Convn n (g1 g2 : 'I_n -> T) (d1 d2 : {fdist 'I_n}) : g1 =1 g2 -> d1 =1 d2 -> <|>_d1 g1 = <|>_d2 g2.
proof: Proof. move=> Hg Hd; apply S1_inj; rewrite !S1_Convn. by apply congr_big => // i _; rewrite Hg Hd. 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