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