proposition: Lemma Convn_perm_1 n (d : {fdist 'I_n}) (g : 'I_n -> A) : <|>_d g = <|>_(fdistI_perm d 1%g) (g \o (1%g : 'S_n)).
proof: Proof. rewrite fdistI_perm1; congr (Convn d _). by rewrite boolp.funeqE => i /=; rewrite perm1. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix fingroup perm) Reals Lra mathcomp(mathcomp_extra Rstruct reals) ssrR Reals_ext realType_ext Ranalysis_ext ssr_ext ssralg_ext logb fdist convex