proposition: Lemma big_fsetD1 (a : I) (A : {fset I}) (F : I -> R) : a \in A -> \big[op/idx]_(i <- A) F i = op (F a) (\big[op/idx]_(i <- A `\ a) F i).
proof: Proof. move=> aA; rewrite (big_fsetID (mem [fset a])); congr (op _ _); last first. by apply: eq_fbigl=> i; rewrite !inE/= andbC. rewrite (_ : [fset _ | _ in _ & _] = [fset a]) ?big_seq_fset1//=. by apply/fsetP=> i; rewrite !inE /= andbC; case: eqP => //->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)