proposition: Lemma mem_std p i : is_std p -> (i \in p) = (i < size p).
proof: Proof. by rewrite /is_std => /perm_mem ->; rewrite mem_iota /= add0n. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass ordtype permcomp