proposition: Lemma bigD1 : forall (I : finType) j (P : pred I) F, P j -> \big[*%M/1]_(i | P i) F i === F j * \big[*%M/1]_(i | P i && (i != j)) F i.
proof: Proof. move=> I j P F Pj; rewrite -> (bigID _ (pred1 j)). apply op_morph; try reflexivity. apply (big_pred1 (P:=fun i => P i && pred1 j i)). by move=> i; rewrite /= andbC; case: eqP => // ->. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq div choice fintype finfun paths Setoid Morphisms OperationClasses bigops