proposition: Lemma big_cat : forall 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. move=> I r1 r2 P F; rewrite -> !(big_mkcond _ P). elim: r1 => [|i r1 IHr1]. by rewrite -> big_nil; rewrite -> op_left_id; reflexivity. by move=> /=; rewrite -> IHr1; apply assoc. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq div choice fintype finfun paths Setoid Morphisms OperationClasses bigops