proposition: Lemma big_scalept_conv_split (T : convType) (I : Type) (r : seq I) (P : pred I) (F G : I -> scaled T) (p : {prob R}) : \ssum_(i <- r | P i) (F i <|p|> G i) = (\ssum_(i <- r | P i) F i) <|p|> \ssum_(i <- r | P i) G i.
proof: Proof. rewrite convptE big_split /=. by do 2 rewrite [in RHS]big_morph_scalept ?scalept0//. 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