proposition: Lemma invstd_is_std p : is_std p -> is_std (invstd p).
proof: Proof. move=> H; apply: (invseq_is_std (t := p)). apply: invseq_sym; exact: invseq_invstd. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass ordtype permcomp