proposition: Lemma axidem : ax_idem T.
proof: Proof. move=> a n d g Ha. set supp := fdist_supp d. set f : 'I_#|supp| -> 'I_n := enum_val. have [x Hx] := fdist_supp_mem d. set f' : 'I_n -> 'I_#|supp| := enum_rank_in Hx. set d' := fdistmap f' d. have -> : d = fdistmap f d'. apply fdist_ext => i /=. rewrite fdistmap_comp fdistmapE /=. case/boolP: (i \in supp) => Hi. - rewrite (bigD1 i) /=; last first. by rewrite !inE /f /f' /= enum_rankK_in. rewrite big1; first by rewrite addr0. move=> j /andP[] /eqP <-. case/boolP: (j \in supp). by move=> Hj; rewrite /f /f' /= enum_rankK_in // eqxx. by rewrite inE negbK => /eqP. - rewrite big_pred0. move: Hi; by rewrite inE negbK => /eqP. move=> j; apply/negP => /eqP Hj. by move: Hi; rewrite -Hj enum_valP. rewrite -axmap. have -> : g \o f = fun=> a. apply funext => i; rewrite /f /= Ha //. by move: (enum_valP i); rewrite inE. by rewrite axconst. 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