proposition: Lemma big_split : forall 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. move=> I r P F1 F2. elim: r => //=; first by symmetry; apply op_left_id. move=> i r; case: (P i)=> Heq; rewrite -> Heq; try reflexivity. rewrite -> !op_assoc; apply op_morph; try reflexivity; rewrite -> right_commut at 1; reflexivity. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq div choice fintype finfun paths Setoid Morphisms OperationClasses bigops