proposition: Lemma pair_big_dep_idem (I J : finType) (P : pred I) (Q : I -> pred J) F : \big[op/x]_(i | P i) \big[op/x]_(j | Q i j) F i j = \big[op/x]_(p | P p.1 && Q p.1 p.2) F p.1 p.2.
proof: Proof. rewrite sig_big_dep_idem; apply: (reindex (fun x => Tagged (fun=> J) x.2)). by exists (fun x => (projT1 x, projT2 x)) => -[]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)