proposition: Lemma size_sdtn (s : stdwordn) : size (val s) = n.
proof: Proof. Proof using. by case: s => s /= /andP[_ /eqP]. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass ordtype permcomp