proposition: Lemma big_fsetU1 (a : I) (A : {fset I}) (F : I -> R) : a \notin A -> \big[op/idx]_(i <- (a |` A)) F i = op (F a) (\big[op/idx]_(i <- A) F i).
proof: Proof. move=> aNA; rewrite eq_big_imfset//= big_map undup_id ?big_cat ?big_seq_fset1//. rewrite cat_uniq ?fset_uniq andbT//=; apply/hasPn=> /= x xA; rewrite !inE/=. by apply: contraNneq aNA => <-. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)