proposition: Lemma psumr_neq0 (I : eqType) (r : seq I) (P : pred I) (F : I -> R) : (forall i, P i -> 0 <= F i) -> (\sum_(i <- r | P i) (F i) != 0) = (has (fun i => P i && (0 < F i)) r).
proof: Proof. move=> F_ge0; rewrite psumr_eq0// -has_predC; apply: eq_has => x /=. by case Px: (P x); rewrite //= lt_def F_ge0 ?andbT. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)