proposition: Lemma big_split I r (P : pred I) (F1 F2 : I -> X) : \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. elim/big_rec3 : _ => [|i x y z Pi ->]; rewrite ?monU //. rewrite -!monA. apply: mon_eqv => //. by rewrite monA [_ ⊗ y]monC monA. Qed.
imports: HB(structures) Coq(RelationClasses Morphisms Relation_Definitions) mathcomp(all_ssreflect)