proposition: Lemma big_split I r (P : pred I) F1 F2 : \big[*%M/1]_(i <- r | P i) (F1 i * F2 i) = \big[*%M/1]_(i <- r | P i) F1 i * \big[*%M/1]_(i <- r | P i) F2 i.
proof: Proof. exact/big_split_idem/mul1m. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)