proposition: Lemma fdist_convn1 (g : 'I_n -> fdist R A) a : fdist_convn (fdist1 a) g = g a.
proof: Proof. apply/fdist_ext => a0; rewrite fdist_convnE (bigD1 a) //= fdist1xx mul1r. by rewrite big1 ?addr0 // => i ia; rewrite fdist10// mul0r. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup perm matrix) mathcomp(all_algebra vector reals normedtype) mathcomp(mathcomp_extra boolp) mathcomp(Rstruct) ssrR logb realType_ext ssr_ext ssralg_ext bigop_ext