proposition: Theorem Convn_fdist_convn (n m : nat) (d : {fdist 'I_n}) (e : 'I_n -> {fdist 'I_m}) (x : 'I_m -> T) : <|>_d (fun i => <|>_(e i) x) = <|>_(fdist_convn d e) x.
proof: Proof. apply S1_inj; rewrite !S1_Convn -[in RHS]big_enum -ssum_fdist_convn. by apply eq_bigr => i _; rewrite big_enum S1_Convn. 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