proposition: Lemma prodR_ge1 (A : finType) f : (forall a, 1 <= f a) -> 1 <= \prod_(a : A) f a.
proof: Proof. elim/big_ind : _ => // [|x y Hx Hy *]. by move=> _; apply/RleP; rewrite lexx. by rewrite -{1}(mulR1 1); apply/leR_pmul => //; [exact: Hx | exact: Hy]. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) Reals mathcomp(lra) mathcomp(Rstruct)