proposition: Lemma invstdK s : is_std s -> invstd (invstd s) = s.
proof: Proof. move=> Hstd; apply: (invseqE (s := invstd s)). - by apply: invseq_invstd; apply: invstd_is_std. - by apply: invseq_sym; apply: invseq_invstd. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass ordtype permcomp