proposition: Lemma equiv_convn n (d : {fdist 'I_n}) g : <&>_d g = <|>_d g.
proof: Proof. elim: n d g => [|n IH d g /=]. by move=> d; move: (fdist_card_neq0 d); rewrite card_ord. case: Bool.bool_dec => [|b]. by rewrite fdist1E1 => /eqP ->; rewrite axproj. rewrite -{}IH. have -> : (fun i => g (fdist_del_idx ord0 i)) = g \o lift ord0. by apply funext => i; rewrite /fdist_del_idx ltn0. apply/esym; rewrite axmap /=. rewrite /(_ <| _ |> _)/= /binconv. set d' := fdistmap _ _. rewrite -(axproj ord0) convn_if axbary. congr (<&>_ _ _); apply fdist_ext => i. rewrite fdist_convnE !big_ord_recl big_ord0 addr0 /= !fdistI2E /=. rewrite fdist1E /d' fdistmapE /=. have [->|] := eqVneq i ord0; first by rewrite big1 // mulr0 mulr1 addr0. case: (unliftP ord0 i) => //= [j|] -> // Hj. rewrite (big_pred1 j) //=. rewrite fdist_delE fdistD1E /= /onem. rewrite mulr0 add0r mulrA (mulrC (1 - d ord0)%R) mulrK //. apply/eqP => /(congr1 (Rplus (d ord0))). rewrite addRCA addRN !addR0 => b'. by elim b; rewrite -b' eqxx. 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