proposition: Lemma bigD1 (I : finType) j (P : pred I) F : P j -> \big[op/x]_(i | P i) F i = op (F j) (\big[op/x]_(i | P i && (i != j)) F i).
proof: Proof. rewrite (big_rem_AC _ _ (mem_index_enum j)) => ->. by rewrite rem_filter ?index_enum_uniq// big_filter_cond big_andbC. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)