proposition: Lemma big_cat I r1 r2 (P : pred I) F : \big[*%M/1]_(i <- r1 ++ r2 | P i) F i = \big[*%M/1]_(i <- r1 | P i) F i * \big[*%M/1]_(i <- r2 | P i) F i.
proof: Proof. rewrite !(big_mkcond _ P) unlock. by elim: r1 => /= [|i r1 ->]; rewrite (mul1m, mulmA). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)