proposition: Lemma CR_cv_unique : forall {R : ConstructiveReals} (xn : nat -> CRcarrier R) (a b : CRcarrier R), CR_cv R xn a -> CR_cv R xn b -> a == b.
proof: Proof. intros. assert (CR_cv R (fun _ => 0) (CRminus R b a)). { apply (CR_cv_extens (fun n => CRminus R (xn n) (xn n))). - intro n. unfold CRminus. apply CRplus_opp_r. - apply CR_cv_plus. + exact H0. + apply CR_cv_opp, H. } assert (forall q r : Q, 0 < q -> / q < r -> 1 < q * r)%Q. { intros. apply (Qmult_lt_l _ _ q) in H3. - rewrite Qmult_inv_r in H3. + exact H3. + intro abs. rewrite abs in H2. exact (Qlt_irrefl 0 H2). - exact H2. } clear H H0 xn. remember (CRminus R b a) as z. assert (z == 0). 1:split. - intro abs. destruct (CR_Q_dense R _ _ abs) as [q [H0 H]]. destruct (Qarchimedean (/(-q))) as [p pmaj]. specialize (H1 p) as [n nmaj]. specialize (nmaj n (Nat.le_refl n)). apply nmaj. apply (CRlt_trans _ (CR_of_Q R (-q))). + apply CR_of_Q_lt. apply H2 in pmaj. * apply (Qmult_lt_r _ _ (1#p)) in pmaj. 2: reflexivity. rewrite Qmult_1_l, <- Qmult_assoc in pmaj. setoid_replace ((Z.pos p # 1) * (1 # p))%Q with 1%Q in pmaj. -- rewrite Qmult_1_r in pmaj. exact pmaj. -- unfold Qeq, Qnum, Qden; simpl. do 2 rewrite Pos.mul_1_r. reflexivity. * apply (Qplus_lt_l _ _ q). ring_simplify. apply (lt_CR_of_Q R q 0). exact H. + apply (CRlt_le_trans _ (CRopp R z)). * apply (CRle_lt_trans _ (CRopp R (CR_of_Q R q))). -- apply CR_of_Q_opp. -- apply CRopp_gt_lt_contravar, H0. * apply (CRle_trans _ (CRabs R (CRopp R z))). -- pose proof (CRabs_def R (CRopp R z) (CRabs R (CRopp R z))) as [_ H1]. apply H1, CRle_refl. -- apply CRabs_morph. unfold CRminus. symmetry. apply CRplus_0_l. - intro abs. destruct (CR_Q_dense R _ _ abs) as [q [H0 H]]. destruct (Qarchimedean (/q)) as [p pmaj]. specialize (H1 p) as [n nmaj]. specialize (nmaj n (Nat.le_refl n)). apply nmaj. apply (CRlt_trans _ (CR_of_Q R q)). + apply CR_of_Q_lt. apply H2 in pmaj. * apply (Qmult_lt_r _ _ (1#p)) in pmaj. 2: reflexivity. rewrite Qmult_1_l, <- Qmult_assoc in pmaj. setoid_replace ((Z.pos p # 1) * (1 # p))%Q with 1%Q in pmaj. -- rewrite Qmult_1_r in pmaj. exact pmaj. -- unfold Qeq, Qnum, Qden; simpl. do 2 rewrite Pos.mul_1_r. reflexivity. * apply (lt_CR_of_Q R 0 q). exact H0. + apply (CRlt_le_trans _ _ _ H). apply (CRle_trans _ (CRabs R (CRopp R z))). * apply (CRle_trans _ (CRabs R z)). -- pose proof (CRabs_def R z (CRabs R z)) as [_ H1]. apply H1. apply CRle_refl. -- apply CRabs_opp. * apply CRabs_morph. unfold CRminus. symmetry. apply CRplus_0_l. - subst z. apply (CRplus_eq_reg_l (CRopp R a)). rewrite CRplus_opp_l, CRplus_comm. symmetry. exact H. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveAbs