proposition: Lemma std_posbig s : posbig (std s) = posbig s.
proof: Proof. Proof using. rewrite /std. case: s => [// | s0 s] /=. case (boolP (allLtn s s0)) => [/= | Hmax] /=. by rewrite take0 drop0 cat0s /= allLtn_std_rec. set pos := (posbig s).+1; set LR := take _ _. have HposLR : pos = size LR. rewrite /LR size_take /pos size_std_rec. case: (ltnP (posbig s).+1 (size s)) => Hpos; first by []. apply/eqP; rewrite eqn_leq Hpos andbT. have: s != [::] by move: Hmax; case s. exact: posbig_size. rewrite HposLR; apply/eqP; rewrite -posbigE. have:= allLtn_std_rec (s0 :: rembig s). rewrite size_take size_std_rec HposLR. have Hif : (if size LR < size s then size LR else size s) = size LR. rewrite /LR /pos size_take size_std_rec. case: (ltnP (posbig s).+1 (size s)) => Hpos; first by rewrite Hpos. by rewrite ltnn. rewrite /LR size_take size_std_rec HposLR !Hif /std. have -> : size (s0 :: rembig s) = size s. by rewrite /= size_rembig; move: Hmax; case s. rewrite -{1}[std_rec _ _](cat_take_drop (size LR)) allLtn_catE => /andP[H1 ->]. by rewrite andbT; exact: allLtnW. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass ordtype permcomp