proposition: Lemma bigID : forall I r (a P : pred I) F, \big[*%M/1]_(i <- r | P i) F i === \big[*%M/1]_(i <- r | P i && a i) F i * \big[*%M/1]_(i <- r | P i && ~~ a i) F i.
proof: Proof. move=> I r a P F. rewrite -> big_mkcond. rewrite -> (big_mkcond _ (fun i => P i && a i)). rewrite -> (big_mkcond _ (fun i => P i && ~~ a i)). rewrite <- big_split; apply eq_bigr => i _. by case: (P i) => //=; case: (a i) => //=; symmetry; try apply op_left_id; apply op_right_id. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq div choice fintype finfun paths Setoid Morphisms OperationClasses bigops