proposition: Lemma stdP (s : seq T) p : reflect (std_spec s p) (std s == p).
proof: Proof. apply/(iffP idP). - by move/eqP <-; exact: std_specP. - by move=> Hspec; apply/eqP; exact: (std_spec_uniq (std_specP s)). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass ordtype permcomp