proposition: Lemma Rabs_triang_gen : forall (An:nat -> R) (N:nat), Rabs (sum_f_R0 An N) <= sum_f_R0 (fun i:nat => Rabs (An i)) N.
proof: Proof. intros. induction N as [| N HrecN]. - simpl. right; reflexivity. - do 2 rewrite tech5. apply Rle_trans with (Rabs (sum_f_R0 An N) + Rabs (An (S N))). + apply Rabs_triang. + do 2 rewrite <- (Rplus_comm (Rabs (An (S N)))). apply Rplus_le_compat_l; apply HrecN. Qed.
imports: Rbase Rfunctions Rseries Rcomplete