proposition: Lemma Convn_cst (a : T) (n : nat) (d : {fdist 'I_n}) : <|>_d (fun=> a) = a.
proof: Proof. elim: n d; first by move=> d; move/fdistI0_False: (d). move=> n IHn d. have [|] := eqVneq (d ord0) 1%coqR; first by move/(Convn_proj (fun=> a)). by move=> d0n0; rewrite ConvnIE IHn convmm. 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