proposition: Lemma Convn_permI1 (d : {fdist 'I_1}) (g : 'I_1 -> A) (s : 'S_1) : <|>_d g = <|>_(fdistI_perm d s) (g \o s).
proof: Proof. have s1 : s = 1%g. apply/permP => i; by case: (s i) => -[|//] ?; rewrite perm1 (ord1 i); exact/val_inj. by rewrite s1 -Convn_perm_1. 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