proposition: Lemma S1_Convn_finType : S1 (<$>_d f) = \ssum_i scalept (d i) (S1 (f i)).
proof: Proof. rewrite /Convn_finType.Convn_finType S1_Convn /=. rewrite (reindex_onto enum_rank enum_val) /=; last by move=> i _; rewrite enum_valK. apply eq_big => /=; first by move=> i; rewrite enum_rankK eqxx. move=> i _; rewrite /Convn_finType.d_enum ffunE. by rewrite enum_rankK. 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