proposition: Lemma axidem : ax_idem T.
proof: Proof. by move=> a n d g Hd; apply axidem => i; move: (Hd i); rewrite inE. 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