proposition: Lemma axmap : ax_map T.
proof: Proof. move=> n m u d g. have -> : fdistmap u d = fdist_convn d (fun i : 'I_m => fdist1 (u i)). by apply: fdist_ext => /= i; rewrite /fdistmap/= fdistbindE// fdist_convnE. rewrite -axbary. by congr (<&>_ _ _); apply funext => i /=; rewrite axproj. 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