proposition: Lemma std_specP (s : seq T) : std_spec s (std s).
proof: Proof. constructor; [exact: std_is_std | exact: eq_inv_std]. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass ordtype permcomp