proposition: Lemma fdistX_self : fdistX (fdist_self P) = fdist_self P.
proof: Proof. apply/fdist_ext => -[a1 a2]. by rewrite fdistXE !fdist_selfE /= eq_sym; case: ifPn => // /eqP ->. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup perm matrix) mathcomp(all_algebra vector reals normedtype) mathcomp(mathcomp_extra boolp) mathcomp(Rstruct) ssrR logb realType_ext ssr_ext ssralg_ext bigop_ext