proposition: Lemma card_stdwordn : #|{:stdwordn}| = n`!.
proof: Proof. Proof using. by rewrite card_subE size_map -card_Sn cardE. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass ordtype permcomp