fact: Definition BoxIn sh rc (rc_sh : in_shape sh rc) : box_in sh := BoxSkew (BoxIn_subproof rc_sh).
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype