proposition: Lemma sig_big_dep (I : finType) (J : I -> finType) (P : pred I) (Q : forall {i}, pred (J i)) (F : forall {i}, J i -> R) : \big[op/idx]_(i | P i) \big[op/idx]_(j : J i | Q j) F j = \big[op/idx]_(p : {i : I & J i} | P (tag p) && Q (tagged p)) F (tagged p).
proof: Proof. exact/sig_big_dep_idem/mul1m. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)