proposition: Lemma tech2 : forall (An:nat -> R) (m n:nat), (m < n)%nat -> sum_f_R0 An n = sum_f_R0 An m + sum_f_R0 (fun i:nat => An (S m + i)%nat) (n - S m).
proof: Proof. intros; induction n as [| n Hrecn]. - elim (Nat.nlt_0_r _ H). - cut ((m < n)%nat \/ m = n). + intro; elim H0; intro. * replace (sum_f_R0 An (S n)) with (sum_f_R0 An n + An (S n)); [ idtac | reflexivity ]. replace (S n - S m)%nat with (S (n - S m)). -- replace (sum_f_R0 (fun i:nat => An (S m + i)%nat) (S (n - S m))) with (sum_f_R0 (fun i:nat => An (S m + i)%nat) (n - S m) + An (S m + S (n - S m))%nat); [ idtac | reflexivity ]. replace (S m + S (n - S m))%nat with (S n). ++ rewrite (Hrecn H1). ring. ++ apply INR_eq; rewrite S_INR; rewrite plus_INR; do 2 rewrite S_INR; rewrite minus_INR. ** rewrite S_INR; ring. ** apply Nat.le_succ_l; assumption. -- apply INR_eq; rewrite S_INR; repeat rewrite minus_INR. ++ repeat rewrite S_INR; ring. ++ apply le_n_S; apply Nat.lt_le_incl; assumption. ++ apply Nat.le_succ_l; assumption. * rewrite H1; rewrite Nat.sub_diag; simpl. replace (n + 0)%nat with n; [ reflexivity | ring ]. + inversion H. * right; reflexivity. * left; apply Nat.lt_le_trans with (S m); [ apply Nat.lt_succ_diag_r | assumption ]. Qed.
imports: Rbase Rfunctions Rseries Rcomplete