proposition: Lemma std_std s : is_std s -> std s = s.
proof: Proof. rewrite /std /is_std. move Hn : (size s) => n; elim: n s Hn => [/= | n IHn] s Hsz. - by move: Hsz=> /eqP/nilP ->. - case Hs : s Hsz => [// | s0 s']. rewrite -{-1}Hs => Hsz Hperm /=. have Hszrem : size (rembig s) = n by rewrite size_rembig Hs Hsz. have Hprem : perm_eq (rembig s) (iota 0 n). by rewrite -rembig_iota; exact: perm_rembig. rewrite (IHn _ Hszrem Hprem) Hs {IHn}. have:= Hperm; rewrite {1}Hs => /maxL_perm. rewrite maxL_iota_n => <-. exact: posbig_take_dropE. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass ordtype permcomp