proposition: Lemma fdistI_perm1 (n : nat) (P : R.-fdist 'I_n) : @fdistI_perm R n P 1%g = P.
proof: Proof. by apply/fdist_ext => /= i; rewrite fdistI_permE perm1. 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