proposition: Lemma serie_not_zero : forall f k, 0 < f k -> 0 < serie f.
proof: Proof. intros; apply Ult_le_trans with (sigma f (S k)). apply (sigma_not_zero f) with (k:=k); auto. unfold serie; apply le_lub; auto. Qed.
imports: ALEA(Utheory)