proposition: Lemma ger0_normed {K : numFieldType} (u_ : K ^nat) : (forall n, 0 <= u_ n) -> [normed series u_] = series u_.
proof: Proof. by move=> u_gt0; rewrite funeqE => n /=; apply: eq_bigr => k; rewrite ger0_norm. Qed.
imports: mathcomp(all_ssreflect ssralg ssrint ssrnum matrix) mathcomp(interval rat) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(set_interval) reals ereal signed topology normedtype landau