proposition: Lemma std_spec_uniq (u : seq T) p q : std_spec u p -> std_spec u q -> p = q.
proof: Proof. case=> Heqp Hp; case=> Heqq /(eq_inv_trans (eq_inv_sym Hp)) {Hp u}. rewrite -{2}(std_std Heqp) -{2}(std_std Heqq). exact: std_eq_inv. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass ordtype permcomp