proposition: Lemma allLtn_std_rec s : allLtn (std s) (size s).
proof: Proof. Proof using. by apply/allP=> i /=; rewrite ltEnat in_std_ltn_size. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass ordtype permcomp