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