proposition: Lemma prodRN (I : finType) (p : pred I) (F : I -> R) : \prod_(i in p) - F i = (-1) ^ #|p| * \prod_(i in p) F i.
proof: Proof. rewrite -prodR_card_constE. apply: (big_rec3 (fun a b c => a = b * c)). { by rewrite mul1R. } move=> i a b c Hi Habc; rewrite Habc; ring. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) Reals mathcomp(lra) mathcomp(Rstruct)