proposition: Lemma sum_f_R0_triangle : forall (x:nat -> R) (n:nat), Rabs (sum_f_R0 x n) <= sum_f_R0 (fun i:nat => Rabs (x i)) n.
proof: Proof. intro; simple induction n; simpl. - unfold Rle; right; reflexivity. - intro m; intro; apply (Rle_trans (Rabs (sum_f_R0 x m + x (S m))) (Rabs (sum_f_R0 x m) + Rabs (x (S m))) (sum_f_R0 (fun i:nat => Rabs (x i)) m + Rabs (x (S m)))). + apply Rabs_triang. + rewrite Rplus_comm; rewrite (Rplus_comm (sum_f_R0 (fun i:nat => Rabs (x i)) m) (Rabs (x (S m)))); apply Rplus_le_compat_l; assumption. Qed.
imports: ArithRing Rdefinitions Raxioms RIneq Rpow_def R_Ifp Rbasic_fun R_sqr SplitAbsolu SplitRmult ArithProp Zpower Ztac