proposition: Lemma bigID2 (R : Type) (I : finType) (J : {set I}) (F1 F2 : I -> R) (idx : R) (op : Monoid.com_law idx) : \big[op/idx]_(j in I) (if j \notin J then F1 j else F2 j) = op (\big[op/idx]_(j in ~: J) F1 j) (\big[op/idx]_(j in J) F2 j).
proof: Proof. rewrite (bigID (mem (setC J)) predT); apply: congr2. by apply: eq_big =>// i /andP [H1 H2]; rewrite inE in_setC in H2; rewrite H2. apply: eq_big => [i|i /andP [H1 H2]] /=; first by rewrite inE negbK. by rewrite ifF //; apply: negbTE; rewrite inE in_setC in H2. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) logb ssr_ext ssralg_ext