proposition: Lemma pair_bigA_idem (I J : finType) (F : I -> J -> R) : \big[op/x]_i \big[op/x]_j F i j = \big[op/x]_p F p.1 p.2.
proof: Proof. exact: pair_big_dep_idem. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)