proposition: Lemma big_enum_box_skew (R : Type) (idx : R) (op : Monoid.law idx) (f : nat -> nat -> R): \big[op/idx]_(b <- enum_box_skew) f b.1 b.2 = \big[op/idx]_(0 <= r < size outer) \big[op/idx]_(nth 0 inner r <= c < nth 0 outer r) f r c.
proof: Proof. Proof using. rewrite /enum_box_skew. rewrite big_flatten /index_iota big_map !subn0; apply eq_bigr => r _. by rewrite big_map; apply eq_bigr. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype