proposition: Lemma uniqueness_sum : forall (An:nat -> R) (l1 l2:R), infinite_sum An l1 -> infinite_sum An l2 -> l1 = l2.
proof: Proof. unfold infinite_sum; intros. case (Req_dec l1 l2); intro. - assumption. - cut (0 < Rabs ((l1 - l2) / 2)); [ intro | apply Rabs_pos_lt ]. + elim (H (Rabs ((l1 - l2) / 2)) H2); intros. elim (H0 (Rabs ((l1 - l2) / 2)) H2); intros. set (N := max x0 x); cut (N >= x0)%nat. * cut (N >= x)%nat. -- intros; assert (H7 := H3 N H5); assert (H8 := H4 N H6). cut (Rabs (l1 - l2) <= Rdist (sum_f_R0 An N) l1 + Rdist (sum_f_R0 An N) l2). ++ intro; assert (H10 := Rplus_lt_compat _ _ _ _ H7 H8); assert (H11 := Rle_lt_trans _ _ _ H9 H10); unfold Rdiv in H11; rewrite Rabs_mult in H11. cut (Rabs (/ 2) = / 2). ** intro; rewrite H12 in H11; assert (H13 := Rplus_half_diag); unfold Rdiv in H13; rewrite H13 in H11. elim (Rlt_irrefl _ H11). ** apply Rabs_right; left; change (0 < / 2); apply Rinv_0_lt_compat; cut (0%nat <> 2%nat); [ intro H20; generalize (lt_INR_0 2 (proj1 (Nat.neq_0_lt_0 2) (Nat.neq_sym 0 2 H20))); unfold INR; intro; assumption | discriminate ]. ++ unfold Rdist; rewrite <- (Rabs_Ropp (sum_f_R0 An N - l1)); rewrite Ropp_minus_distr. replace (l1 - l2) with (l1 - sum_f_R0 An N + (sum_f_R0 An N - l2)); [ idtac | ring ]. apply Rabs_triang. -- unfold ge; unfold N; apply Nat.le_max_r. * unfold ge; unfold N; apply Nat.le_max_l. + unfold Rdiv; apply prod_neq_R0. * apply Rminus_eq_contra; assumption. * apply Rinv_neq_0_compat; discrR. Qed.
imports: Rbase Rfunctions Rseries Rcomplete