proposition: Lemma prodR_eq0 (A : finType) (p : pred A) (F : A -> R) : (exists2 i : A, p i & F i = 0%R) <-> \prod_(i : A | p i) F i = 0%R.
proof: Proof. split. { by case => [i Hi Hi0]; rewrite (bigD1 i) //= Hi0 mul0R. } apply big_ind. - by move=> K; exfalso; auto with real. - by move=> ? ? ? ?; rewrite mulR_eq0 => -[]; tauto. - by move=> i Hi Hi0; exists i. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) Reals mathcomp(lra) mathcomp(Rstruct)