proposition: Lemma fdistI_permM (n : nat) (P : R.-fdist 'I_n) (s s' : 'S_n) : @fdistI_perm R n (fdistI_perm P s) s' = fdistI_perm P (s' * s).
proof: Proof. by apply/fdist_ext => /= i; rewrite !fdistI_permE permM. 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