proposition: Lemma fdistXE a b : fdistX (b, a) = P (a, b).
proof: Proof. by rewrite fdistmapE /= -/(swap (a, b)) (big_pred1_inj (bij_inj bij_swap)). 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