proposition: Lemma S1_proj_Convn_finType : S1 (prj (<$>_d f)) = \ssum_i scalept (d i) (S1 (prj (f i))).
proof: Proof. by rewrite Convn_comp; exact: S1_Convn_finType. 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