proposition: Lemma invseq_invstd s : is_std s -> invseq s (invstd s).
proof: Proof. move=> Hstd; rewrite /invseq. apply/andP; split; apply/linvseqP; rewrite size_mkseq => i Hi. - rewrite nth_mkseq. + by apply: (index_uniq _ Hi); apply: std_uniq. + by rewrite -(mem_std _ Hstd) mem_nth. - by rewrite nth_mkseq //=; apply: nth_index; rewrite (mem_std _ Hstd). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass ordtype permcomp