proposition: Lemma card_box_skew : #|{: box_skew}| = sumn (outer / inner).
proof: Proof. Proof using. rewrite card_subE /enum_box_skew size_allpairs_dep; congr sumn. apply: (eq_from_nth (x0 := 0)); rewrite size_map size_iota ?size_diff_shape // => i ltisz. by rewrite (nth_map 0) size_iota // nth_iota // add0n nth_diff_shape. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype