proposition: Lemma fdist_convn_add n m p (g : 'I_(n + m) -> T) (d : {fdist 'I_n}) (e : {fdist 'I_m}) : <|>_(fdist_add d e p) g = <|>_d (g \o @lshift n m) <| p |> <|>_e (g \o @rshift n m).
proof: Proof. apply: S1_inj; rewrite affine_conv/= !S1_Convn convptE big_split_ord/=. do 2 rewrite [in RHS]big_morph_scalept ?scalept0//. congr addpt; apply eq_bigr => i _; rewrite (scaleptA _ _ (S1 _)) //; by rewrite fdist_addE (split_lshift, split_rshift). Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg fingroup perm matrix) mathcomp(mathcomp_extra boolp classical_sets Rstruct) mathcomp(ssrnum ereal) mathcomp(lra Rstruct reals) Reals ssrR Reals_ext Ranalysis_ext ssr_ext ssralg_ext logb realType_ext fdist