proposition: Lemma convn_convnfdist n (g : 'I_n -> {fdist A}) (d : {fdist 'I_n}) : <|>_d g = fdist_convn d g.
proof: Proof. elim: n g d => /= [g d|n IH g d]; first by move: (fdistI0_False d). case: Bool.bool_dec => [/eqP|/Bool.eq_true_not_negb] H. apply/fdist_ext => a. rewrite fdist_convnE big_ord_recl H mul1r big1 ?addr0 //= => j _. by move/eqP/fdist1P : H => -> //; rewrite ?mul0r. apply/fdist_ext => a. rewrite fdist_convE fdist_convnE /= big_ord_recl; congr (_ + _)%coqR. rewrite IH fdist_convnE big_distrr /=; apply eq_bigr => i _. rewrite fdist_delE fdistD1E eq_sym (negbTE (neq_lift _ _)). by rewrite mulrAC mulrC !mulrA mulrV ?mul1r //; exact/onem_neq0. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix fingroup perm) Reals Lra mathcomp(mathcomp_extra Rstruct reals) ssrR Reals_ext realType_ext Ranalysis_ext ssr_ext ssralg_ext logb fdist convex