proposition: Lemma big_box_skew R (idx : R) (op : Monoid.com_law idx) (f : nat * nat -> R): \big[op/idx]_(b : box_skew) f b = \big[op/idx]_(b <- enum_box_skew) f b.
proof: Proof. Proof using. by rewrite -enum_box_skewE big_map /= big_enum. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype