proposition: Lemma tech11 : forall (An Bn Cn:nat -> R) (N:nat), (forall i:nat, An i = Bn i - Cn i) -> sum_f_R0 An N = sum_f_R0 Bn N - sum_f_R0 Cn N.
proof: Proof. intros; induction N as [| N HrecN]. - simpl; apply H. - do 3 rewrite tech5; rewrite HrecN; rewrite (H (S N)); ring. Qed.
imports: Rbase Rfunctions Rseries Rcomplete