proposition: Lemma std_rembig s : std (rembig s) = rembig (std s).
proof: Proof. Proof using. rewrite /std. elim: s => [// | s0 s IHs] /=. case (boolP (allLtn s s0)) => [_ | Hmax]. - case H : (std_rec (size s) s) => [// | t0 t]. by rewrite -H rembig_ins_std. - case H : s IHs Hmax => [// |s1 s']; rewrite -H => IHs Hmax. have <- : size (s0 :: rembig s) = size s by rewrite /= size_rembig H. by have:= rembig_ins_std; rewrite /std => ->. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass ordtype permcomp