proposition: Lemma fdist_permE v : fdist_perm v = P (col_perm s v).
proof: Proof. rewrite fdistmapE /= {1}(_ : v = col_perm s^-1 (col_perm s v)); last first. by rewrite -col_permM mulVg col_perm1. rewrite big_pred1_inj //; exact: col_perm_inj. 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