proposition: Lemma big_pairA (F : I * J -> R): \big[op/idx]_p F p = \big[op/idx]_i \big[op/idx]_j F (i, j).
proof: Proof. exact: (big_pair_dep xpredT xpredT). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset order) mathcomp(ssralg)