proposition: Lemma big_rem (I : eqType) r x (P : pred I) F : x \in r -> \big[*%M/1]_(y <- r | P y) F y = (if P x then F x else 1) * \big[*%M/1]_(y <- rem x r | P y) F y.
proof: Proof. by move/perm_to_rem/(perm_big _)->; rewrite !(big_mkcond _ _ P) big_cons. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)