proposition: Lemma Convn_permI3 (d : {fdist 'I_3}) (g : 'I_3 -> A) (s : 'S_3) : <|>_d g = <|>_(fdistI_perm d s) (g \o s).
proof: Proof. move: s d g. apply: S3.suff_generators; last first. move=> s s' Hs Hs' d g. rewrite Hs Hs' fdistI_permM; congr (Convn _ _). by rewrite boolp.funeqE => i /=; rewrite permE. exact: Convn_permI3_p02. exact: Convn_permI3_p01. exact: 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