proposition: Lemma leR_prodR (A : finType) f g : (forall a, 0 <= f a <= g a) -> \prod_a f a <= \prod_(a : A) g a.
proof: Proof. move=> fg. have [/forallP Hf|] := boolP [forall i, f i != 0%R]; last first. rewrite negb_forall => /existsP[i0 /negPn/eqP fi0]. rewrite (bigD1 i0) //= fi0 mul0R; apply prodR_ge0. by move=> i ; move: (fg i) => [Hi1 Hi2]; exact: (leR_trans Hi1 Hi2). have Hprodf : 0 < \prod_(i : A) f i. apply/RltP. apply prodr_gt0 => a _. apply/RltP. move: (Hf a) (fg a) => {}Hf {fg}[Hf2 _]. by apply/RltP; rewrite lt0r Hf/=; exact/RleP. apply (@leR_pmul2r (1 * / \prod_(i : A) f i) _ _). apply divR_gt0 => //; lra. rewrite mul1R mulRV; last exact/gtR_eqF. set inv_spec := fun r => if r == 0 then 0 else / r. rewrite (_ : / (\prod_(a : A) f a) = inv_spec (\prod_(a : A) f a)); last first. rewrite /inv_spec (_ : \prod_(a : A) f a == 0 = false) //. exact/negbTE/gtR_eqF. rewrite (@big_morph _ _ (inv_spec) R1 Rmult R1 Rmult _); last 2 first. - move=> a b /=. case/boolP : ((a != 0) && (b != 0)). + move=> /andP [/negbTE Ha /negbTE Hb]; rewrite /inv_spec Ha Hb. move/negbT in Ha ; move/negbT in Hb. have -> : (a * b)%R == 0 = false by rewrite mulR_eq0' (negbTE Ha) (negbTE Hb). by rewrite invRM //; exact/eqP. + rewrite negb_and !negbK => /orP[|]/eqP ->; by rewrite /inv_spec !(eqxx,mul0R,mulR0). - by rewrite /inv_spec ifF ?invR1 //; exact/negbTE/eqP/R1_neq_R0. rewrite -big_split /=; apply prodR_ge1 => a. move/(_ a) in Hf. move: fg => /(_ a) [Hf2 fg]. rewrite /inv_spec. move/negbTE in Hf; rewrite Hf; move/negbT in Hf. rewrite -(mulRV (f a)) //. apply leR_wpmul2r => //. rewrite -(mul1R (/ f a)). by apply divR_ge0; [Lra.lra |by apply/RltP; rewrite lt0r Hf; exact/RleP]. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) Reals mathcomp(lra) mathcomp(Rstruct)