proposition: Lemma big_rem_AC (I : eqType) (r : seq I) z (P : pred I) F : z \in r -> \big[op/x]_(y <- r | P y) F y = if P z then op (F z) (\big[op/x]_(y <- rem z r | P y) F y) else \big[op/x]_(y <- rem z r | P y) F y.
proof: Proof. elim: r =>// i r ih; rewrite big_cons rem_cons inE =>/predU1P[-> /[!eqxx]//|zr]. by case: eqP => [-> //|]; rewrite ih// big_cons; case: ifPn; case: ifPn. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)