proposition: Lemma is_stdP s : reflect (forall n, n < size s -> n \in s) (is_std s).
proof: Proof. rewrite /is_std; apply (iffP idP). - by move=> Hperm n Hn; rewrite (perm_mem Hperm) mem_iota add0n Hn. - move=> H. have Hsubs : {subset iota 0 (size s) <= s}. by move=> n; rewrite mem_iota /= add0n; apply: H. have Hsz : size s <= size (iota 0 (size s)) by rewrite size_iota. have [_ Hs]:= uniq_min_size (iota_uniq _ _) Hsubs Hsz. have Huniq:= leq_size_uniq (iota_uniq _ _) Hsubs Hsz. apply (uniq_perm Huniq (iota_uniq _ _)). by move => i; rewrite Hs. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass ordtype permcomp