proposition: Lemma big_split_idem I r (P : pred I) F1 F2 : \big[op/x]_(i <- r | P i) op (F1 i) (F2 i) = op (\big[op/x]_(i <- r | P i) F1 i) (\big[op/x]_(i <- r | P i) F2 i).
proof: Proof. by elim/big_rec3: _ => [|i x' y _ _ ->]; rewrite ?opxx// opCA -!opA opCA. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)