proposition: Lemma invseq_is_std s t : invseq s t -> is_std s.
proof: Proof. move=> /invseq_sym Hinv; rewrite /is_std perm_sym. apply: perm_size_uniq. - exact: iota_uniq. - rewrite -(size_invseq Hinv); apply: linvseq_subset_iota. by move: Hinv; rewrite /invseq => /andP[]. - by rewrite size_iota. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass ordtype permcomp