proposition: Lemma big_setU1 a A F : a \notin A -> \big[aop/idx]_(i in a |: A) F i = aop (F a) (\big[aop/idx]_(i in A) F i).
proof: Proof. by move=> notAa; rewrite (@big_setD1 a) ?setU11 //= setU1K. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)