proposition: Lemma Convn_perm (n : nat) (d : {fdist 'I_n}) (g : 'I_n -> A) (s : 'S_n) : <|>_d g = <|>_(fdistI_perm d s) (g \o s).
proof: Proof. move: d g s. elim: n.+1 {-2}n (ltnSn n) => {n} // m IH n nm d g s. destruct n as [|n]; first by move: (fdistI0_False d). destruct n as [|n]; first exact: Convn_permI1. destruct n as [|n]; first exact: Convn_permI2. destruct n as [|n]; first exact: Convn_permI3. move: m IH nm d g. apply (@Sn.suff_generators _ (fun s => forall m : nat, (forall n0, (n0 < m)%nat -> forall (d : {fdist 'I_n0}) (g : 'I_n0 -> A) (s0 : 'S_n0), <|>_d g = <|>_(fdistI_perm d s0) (g \o s0)) -> (n.+4 < m.+1)%nat -> forall (d : {fdist 'I_n.+4}) (g : 'I_n.+4 -> A), <|>_d g = <|>_(fdistI_perm d s) (g \o s))). - move=> s1 s2 H1 H2 m IH nm d g. rewrite (H1 m) // (H2 m) // fdistI_permM; congr (Convn _ _). by rewrite boolp.funeqE => i; rewrite /= permM. - move=> m IH nm d g. have [/eqP|dmax1] := eqVneq (d ord0) 1%coqR. rewrite fdist1E1 => /eqP ->. by rewrite Convn_fdist1 fdistI_perm_fdist1 Convn_fdist1 /= permKV. by apply Convn_perm_tperm with m. - move=> {}s H. move=> m IH nm d g. have [/eqP|dmax1] := eqVneq (d ord0) 1%coqR. rewrite fdist1E1 => /eqP ->. by rewrite Convn_fdist1 fdistI_perm_fdist1 Convn_fdist1 /= permKV. by apply Convn_perm_projection with m. 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