proposition: Lemma is_std_wordpermP s : reflect (exists p : 'S_(size s), s = wordperm p) (is_std s).
proof: Proof. apply: (iffP idP). + by move/perm_of_std => [p Hp]; exists p. + by move=> [p ->]; apply: wordperm_std. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass ordtype permcomp