proposition: Lemma sum_eq : forall (An Bn:nat -> R) (N:nat), (forall i:nat, (i <= N)%nat -> An i = Bn i) -> sum_f_R0 An N = sum_f_R0 Bn N.
proof: Proof. intros; induction N as [| N HrecN]. - simpl; apply H; apply le_n. - do 2 rewrite tech5; rewrite HrecN. + rewrite (H (S N)); [ reflexivity | 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