proposition: Lemma sumR_neq0 (U : eqType) (P : U -> R) (s : seq.seq U) : (forall i, 0 <= P i) -> \sum_(a0 <- s) P a0 != 0 <-> exists i : U, i \in s /\ 0 < P i.
proof: Proof. move=> /(_ _) /RleP P0. rewrite sumRE psumr_neq0 //. under eq_has do rewrite andTb. split; first by move=> /hasP [x xs /RltP Px0]; exists x; split. by case=> x [] xs /RltP Px0; apply/hasP; exists x. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) Reals mathcomp(lra) mathcomp(Rstruct)