proposition: Lemma axpart : ax_part T.
proof: Proof. move=> n m K d g; rewrite axbary; congr (<&>_ _ _). by apply fdist_ext => /= j; rewrite !fdistE -FDistPart.dK. 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