proposition: Lemma axidem : ax_idem T.
proof: Proof. move=> a n d g Hd. have /=[k Hk] := fdist_supp_mem d. have -> : g = (fun i => <&>_(fdist1 (if i \in fdist_supp d then k else i)) g). apply funext => i; rewrite axproj. case: ifP => // /Hd ->; by rewrite (Hd k). rewrite axbary (_ : fdist_convn _ _ = fdist1 k) ?axproj ?Hd //. apply fdist_ext => /= i. rewrite fdist_convnE sum_fdist_supp fdistE. under eq_bigr => j /= -> do rewrite fdistE. by rewrite -sum_fdist_supp -big_distrl FDist.f1 /= mul1r. 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