proposition: Lemma big_cat (I : eqType) (r1 r2 : seq I) (P : pred I) (F : I -> X) : \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). elim: r1 => /= [|i r1 IH]; first by rewrite big_nil monUl. by rewrite !big_cons IH monA. Qed.
imports: HB(structures) Coq(RelationClasses Morphisms Relation_Definitions) mathcomp(all_ssreflect)