proposition: Lemma sum_eq_R0 : forall (An:nat -> R) (N:nat), (forall n:nat, (n <= N)%nat -> An n = 0) -> sum_f_R0 An N = 0.
proof: Proof. intros; induction N as [| N HrecN]. - simpl; apply H; apply le_n. - rewrite tech5; rewrite HrecN; [ rewrite Rplus_0_l; apply H; apply le_n | intros; apply H; apply Nat.le_trans with N; [ assumption | apply Nat.le_succ_diag_r ] ]. Qed.
imports: Rbase Rfunctions Rseries Rcomplete