proposition: Lemma fdist_convn_Add (R : realType) (n m : nat) (d1 : {fdist 'I_n}) (d2 : {fdist 'I_m}) (p : {prob R}) (A : finType) (g : 'I_n -> {fdist A}) (h : 'I_m -> {fdist A}) : fdist_convn (fdist_add d1 d2 p) [ffun i => match fintype.split i with inl a => g a | inr a => h a end] = (fdist_convn d1 g <| p |> fdist_convn d2 h)%fdist.
proof: Proof. apply/fdist_ext => a; rewrite !fdist_convE !fdist_convnE. rewrite 2!big_distrr /= big_split_ord /=; congr (_ + _); apply eq_bigr => i _; rewrite fdist_addE ffunE. case: splitP => /= j ij. rewrite mulrA; congr (_ * d1 _ * (g _) a); exact/val_inj. move: (ltn_ord i); by rewrite ij -ltn_subRL subnn ltn0. case: splitP => /= j ij. move: (ltn_ord j); by rewrite -ij -ltn_subRL subnn ltn0. move/eqP : ij; rewrite eqn_add2l => /eqP ij. rewrite mulrA; congr (_ * d2 _ * (h _) a); exact/val_inj. 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