proposition: Lemma Convn_permI2 (d : {fdist 'I_2}) (g : 'I_2 -> A) (s : 'S_2) : <|>_d g = <|>_(fdistI_perm d s) (g \o s).
proof: Proof. have [->|Hs] := S2.generators s. rewrite fdistI_perm1; congr Convn. by rewrite boolp.funeqE => i; rewrite /= perm1. move: (FDist.ge0 d ord0); rewrite le0r => /orP -[/eqP /esym d00|d00]. have d11 : d (Ordinal (erefl (1 < 2)%nat)) = 1. rewrite -(FDist.f1 d) 2!big_ord_recl big_ord0 addr0 -d00 add0r; f_equal; exact/val_inj. have H1 : d = fdist1 (Ordinal (erefl (1 < 2)%nat)). rewrite -fdistI20; apply/fdist_ext => /= i. rewrite fdistI2E; case: ifPn => [/eqP ->//|/= i0]. rewrite onem0 -(FDist.f1 d) 2!big_ord_recl big_ord0 addr0 -d00 add0r; congr (d _). by case: i i0 => -[//|] -[|//] //= i12 _; exact/val_inj. rewrite {1}H1 Convn_fdist1 {1}Hs. have H2 : fdistI_perm d (tperm ord0 (Ordinal (erefl (1 < 2)%nat))) = fdist1 ord0. apply/fdist_ext => /= i; rewrite fdistI_permE fdist1E. have [->|i0] := eqVneq i ord0; first by rewrite permE /= d11. rewrite permE /= (negbTE i0). by case: ifPn => //; case: i i0 => -[|[|]]. by rewrite H2 Convn_fdist1 /=; congr g; rewrite Hs permE /=. have [d10|d10] := eqVneq (d (lift ord0 ord0)) 0%coqR. have d01 : d ord0 = 1. rewrite -(FDist.f1 d) !big_ord_recl big_ord0 addr0. by rewrite addrC -subR_eq subRR d10. have -> : d = fdist1 ord0 by apply/eqP; rewrite -fdist1E1; exact/eqP. by rewrite Convn_fdist1 {1}Hs fdistI_tperm Convn_fdist1 /= Hs permE. rewrite convn2E. rewrite convn2E. rewrite /= Hs permE /= convC !permE /=; congr (_ <| _ |> _); apply val_inj => /=. rewrite fdistI_permE permE /= /onem -(FDist.f1 d) !big_ord_recl big_ord0. by rewrite addr0 (addrC (d ord0)) addrK; congr (d _); exact/val_inj. 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