proposition: Lemma fdist_convn_cst (e : R.-fdist 'I_n) (a : R.-fdist A) : fdist_convn e (fun=> a) = a.
proof: Proof. by apply/fdist_ext => ?; rewrite fdist_convnE -big_distrl /= FDist.f1 mul1r. 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