proposition: Lemma bigD1_seq (I : eqType) (r : seq I) j F : j \in r -> uniq r -> \big[op/x]_(i <- r) F i = op (F j) (\big[op/x]_(i <- r | i != j) F i).
proof: Proof. by move=> /big_rem_AC-> /rem_filter->; rewrite big_filter. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)