proposition: Lemma sumR_gt0 (A : finType) (f : A -> R) (HA : (0 < #|A|)%nat) : (forall a, 0 < f a) -> 0 < \sum_(a in A) f a.
proof: Proof. move=> f0; rewrite ltR_neqAle; split; last first. apply/RleP; rewrite sumRE. by apply/sumr_ge0 => a _; apply/RleP/ltRW. apply/nesym/eqP/sumR_neq0; last by move/card_gt0P : HA => [a _]; exists a. by move=> a; apply/ltRW/f0. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) Reals mathcomp(lra) mathcomp(Rstruct)