proposition: Lemma UL_sequence : forall (Un:nat -> R) (l1 l2:R), Un_cv Un l1 -> Un_cv Un l2 -> l1 = l2.
proof: Proof. intros Un l1 l2; unfold Un_cv; unfold Rdist; intros. apply cond_eq. intros; cut (0 < eps / 2); [ intro | unfold Rdiv; apply Rmult_lt_0_compat; [ assumption | apply Rinv_0_lt_compat; prove_sup0 ] ]. elim (H (eps / 2) H2); intros. elim (H0 (eps / 2) H2); intros. set (N := max x x0). apply Rle_lt_trans with (Rabs (l1 - Un N) + Rabs (Un N - l2)). - replace (l1 - l2) with (l1 - Un N + (Un N - l2)); [ apply Rabs_triang | ring ]. - rewrite <-(Rplus_half_diag eps); apply Rplus_lt_compat. + rewrite <- Rabs_Ropp; rewrite Ropp_minus_distr; apply H3; unfold ge, N; apply Nat.le_max_l. + apply H4; unfold ge, N; apply Nat.le_max_r. Qed.
imports: Rbase Rfunctions Rseries Lia