proposition: Lemma convn_if A n (p : A -> bool) (d1 d2 : {fdist 'I_n}) (g : _ -> T): (fun x => if p x then <&>_d1 g else <&>_d2 g) = (fun x => <&>_(if p x then d1 else d2) g).
proof: Proof. apply funext => x; by rewrite (fun_if (fun d => <&>_d g)). Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum fingroup perm matrix) mathcomp(mathcomp_extra boolp classical_sets) Reals mathcomp(Rstruct reals) ssrR Reals_ext realType_ext Ranalysis_ext ssr_ext ssralg_ext fdist jfdist_cond fsdist convex