proposition: Lemma prodrN (I : finType) (A : pred I) (F : I -> R) : \prod_(i in A) - F i = (- 1) ^+ #|A| * \prod_(i in A) F i.
proof: Proof. rewrite -sum1_card; elim/big_rec3: _ => [|i x n _ _ ->]; first by rewrite mulr1. by rewrite exprS !mulrA mulN1r !mulNr commrX //; apply: commrN1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)