proposition: Lemma std_stdE (disp : unit) (T : orderType disp) (s : seq T) : std (std s) = std s.
proof: Proof. apply: std_std; exact: std_is_std. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass ordtype permcomp