proposition: Lemma mem_enum_box_in sh : enum_box_in sh =i in_shape sh.
proof: Proof. move=> rc; rewrite mem_enum_box_skew. by rewrite !unfold_in -/(in_skew [::] _ rc) in_skewE in_shape_nil /=. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype