proposition: Lemma tech1 : forall (An:nat -> R) (N:nat), (forall n:nat, (n <= N)%nat -> 0 < An n) -> 0 < sum_f_R0 An N.
proof: Proof. intros; induction N as [| N HrecN]. - simpl; apply H; apply le_n. - simpl; apply Rplus_lt_0_compat. + apply HrecN; intros; apply H; apply le_S; assumption. + apply H; apply le_n. Qed.
imports: Rbase Rfunctions Rseries Rcomplete