proposition: Lemma std_max s0 s : is_std (s0 :: s) -> maxL s0 s = size s.
proof: Proof. by rewrite /is_std => /= /maxL_perm /= ->; rewrite maxL_iota_n. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass ordtype permcomp