fact: Structure box_skew : Set := BoxSkew {box_skewval :> nat * nat; _ : in_skew inner outer box_skewval}.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype