proposition: Lemma in_std_ltn_size s i : i \in std s = (i < size s).
proof: Proof. Proof using. by rewrite (mem_std _ (std_is_std s)) size_std_rec. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass ordtype permcomp