proposition: Lemma big_setD1 a A F : a \in A -> \big[aop/idx]_(i in A) F i = aop (F a) (\big[aop/idx]_(i in A :\ a) F i).
proof: Proof. move=> Aa; rewrite (bigD1 a Aa); congr (aop _). by apply: eq_bigl => x; rewrite !inE andbC. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)