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