diff options
Diffstat (limited to 'theories/Reals/Cauchy/ConstructiveRcomplete.v')
| -rw-r--r-- | theories/Reals/Cauchy/ConstructiveRcomplete.v | 384 |
1 files changed, 132 insertions, 252 deletions
diff --git a/theories/Reals/Cauchy/ConstructiveRcomplete.v b/theories/Reals/Cauchy/ConstructiveRcomplete.v index 51fd0dd7f9..6f36e888ed 100644 --- a/theories/Reals/Cauchy/ConstructiveRcomplete.v +++ b/theories/Reals/Cauchy/ConstructiveRcomplete.v @@ -47,44 +47,6 @@ Proof. intros. apply (seq_cv_proper un y). exact H0. symmetry. exact H. Qed. -Lemma growing_transit : forall un : nat -> CReal, - (forall n:nat, un n <= un (S n)) - -> forall n p : nat, le n p -> un n <= un p. -Proof. - induction p. - - intros. inversion H0. apply CRealLe_refl. - - intros. apply Nat.le_succ_r in H0. destruct H0. - apply (CReal_le_trans _ (un p)). apply IHp, H0. apply H. - subst n. apply CRealLe_refl. -Qed. - -Lemma growing_infinite : forall un : nat -> nat, - (forall n:nat, lt (un n) (un (S n))) - -> forall n : nat, le n (un n). -Proof. - induction n. - - apply le_0_n. - - specialize (H n). unfold lt in H. - apply (le_trans _ (S (un n))). apply le_n_S, IHn. exact H. -Qed. - -Lemma Un_cv_growing : forall (un : nat -> CReal) (l : CReal), - (forall n:nat, un n <= un (S n)) - -> (forall n:nat, un n <= l) - -> (forall p : positive, { n : nat | l - un n <= inject_Q (1#p) }) - -> seq_cv un l. -Proof. - intros. intro p. - specialize (H1 p) as [n nmaj]. exists n. - intros. rewrite CReal_abs_minus_sym, CReal_abs_right. - apply (CReal_le_trans _ (l - un n)). apply CReal_plus_le_compat_l. - apply CReal_opp_ge_le_contravar. - exact (growing_transit _ H n i H1). exact nmaj. - rewrite <- (CReal_plus_opp_r (un i)). apply CReal_plus_le_compat. - apply H0. apply CRealLe_refl. -Qed. - - (* Sharpen the archimedean property : constructive versions of the usual floor and ceiling functions. *) @@ -157,15 +119,6 @@ Proof. unfold Qeq; simpl. rewrite Pos.mul_1_r, Z.mul_1_r. reflexivity. Qed. -Definition RQ_limit : forall (x : CReal) (n:nat), - { q:Q & x < inject_Q q < x + inject_Q (1 # Pos.of_nat n) }. -Proof. - intros x n. apply (FQ_dense x (x + inject_Q (1 # Pos.of_nat n))). - rewrite <- (CReal_plus_0_r x). rewrite CReal_plus_assoc. - apply CReal_plus_lt_compat_l. rewrite CReal_plus_0_l. apply inject_Q_lt. - reflexivity. -Qed. - Lemma Qabs_Rabs : forall q : Q, inject_Q (Qabs q) == CReal_abs (inject_Q q). Proof. @@ -176,173 +129,86 @@ Proof. apply inject_Q_le, H. Qed. -Definition Un_cauchy_Q (xn : nat -> Q) : Set - := forall n : positive, - { k : nat | forall p q : nat, le k p -> le k q - -> (Qabs (xn p - xn q) <= 1#n)%Q }. - -Lemma CReal_smaller_interval : forall a b c d : CReal, - a <= c -> c <= b - -> a <= d -> d <= b - -> CReal_abs (d - c) <= b-a. -Proof. - intros. apply CReal_abs_le. split. - - apply (CReal_plus_le_reg_l (b+c)). ring_simplify. - apply CReal_plus_le_compat; assumption. - - apply (CReal_plus_le_reg_l (a+c)). ring_simplify. - apply CReal_plus_le_compat; assumption. -Qed. - -Lemma Rdiag_cauchy_sequence : forall (xn : nat -> CReal), - Un_cauchy_mod xn - -> Un_cauchy_Q (fun n:nat => let (l,_) := RQ_limit (xn n) n in l). -Proof. - intros xn H p. specialize (H (2 * p)%positive) as [k cv]. - exists (max k (2 * Pos.to_nat p)). intros. - specialize (cv p0 q - (le_trans _ _ _ (Nat.le_max_l _ _) H) - (le_trans _ _ _ (Nat.le_max_l _ _) H0)). - destruct (RQ_limit (xn p0) p0) as [r rmaj]. - destruct (RQ_limit (xn q) q) as [s smaj]. - apply Qabs_Qle_condition. split. - - apply le_inject_Q. unfold Qminus. - apply (CReal_le_trans _ (xn p0 - (xn q + inject_Q (1 # 2 * p)))). - + unfold CReal_minus. rewrite CReal_opp_plus_distr. - rewrite <- CReal_plus_assoc. - apply (CReal_plus_le_reg_r (xn q - xn p0 - inject_Q (-(1#p)))). - ring_simplify. unfold CReal_minus. do 2 rewrite <- opp_inject_Q. - rewrite <- inject_Q_plus. - setoid_replace (- - (1 # p) + - (1 # 2 * p))%Q with (1 # 2 * p)%Q. - rewrite CReal_abs_minus_sym in cv. - exact (CReal_le_trans _ _ _ (CReal_le_abs _ ) cv). - rewrite Qopp_involutive. - setoid_replace (1#p)%Q with (2 # 2 *p)%Q. rewrite Qinv_minus_distr. - reflexivity. reflexivity. - + rewrite inject_Q_plus. apply CReal_plus_le_compat. - apply CRealLt_asym. - destruct (RQ_limit (xn p0) p0); simpl. apply rmaj. - apply CRealLt_asym. - rewrite opp_inject_Q. apply CReal_opp_gt_lt_contravar. - destruct smaj. apply (CReal_lt_le_trans _ _ _ c0). - apply CReal_plus_le_compat_l. apply inject_Q_le. - apply Z2Nat.inj_le. discriminate. discriminate. - simpl. assert ((Pos.to_nat p~0 <= q)%nat). - { apply (le_trans _ (Init.Nat.max k (2 * Pos.to_nat p))). - 2: apply H0. replace (p~0)%positive with (2*p)%positive. - 2: reflexivity. rewrite Pos2Nat.inj_mul. - apply Nat.le_max_r. } - rewrite Nat2Pos.id. apply H1. intro abs. subst q. - inversion H1. pose proof (Pos2Nat.is_pos (p~0)). - rewrite H3 in H2. inversion H2. - - apply le_inject_Q. unfold Qminus. - apply (CReal_le_trans _ (xn p0 + inject_Q (1 # 2 * p) - xn q)). - + rewrite inject_Q_plus. apply CReal_plus_le_compat. - apply CRealLt_asym. - destruct (RQ_limit (xn p0) p0); unfold proj1_sig. - apply (CReal_lt_le_trans _ (xn p0 + inject_Q (1 # Pos.of_nat p0))). - apply rmaj. apply CReal_plus_le_compat_l. apply inject_Q_le. - apply Z2Nat.inj_le. discriminate. discriminate. - simpl. assert ((Pos.to_nat p~0 <= p0)%nat). - { apply (le_trans _ (Init.Nat.max k (2 * Pos.to_nat p))). - 2: apply H. replace (p~0)%positive with (2*p)%positive. - 2: reflexivity. rewrite Pos2Nat.inj_mul. - apply Nat.le_max_r. } - rewrite Nat2Pos.id. apply H1. intro abs. subst p0. - inversion H1. pose proof (Pos2Nat.is_pos (p~0)). - rewrite H3 in H2. inversion H2. - apply CRealLt_asym. - rewrite opp_inject_Q. apply CReal_opp_gt_lt_contravar. - destruct (RQ_limit (xn q) q); simpl. apply smaj. - + unfold CReal_minus. rewrite (CReal_plus_comm (xn p0)). - rewrite CReal_plus_assoc. - apply (CReal_plus_le_reg_l (- inject_Q (1 # 2 * p))). - rewrite <- CReal_plus_assoc. rewrite CReal_plus_opp_l. rewrite CReal_plus_0_l. - rewrite <- opp_inject_Q. rewrite <- inject_Q_plus. - setoid_replace (- (1 # 2 * p) + (1 # p))%Q with (1 # 2 * p)%Q. - exact (CReal_le_trans _ _ _ (CReal_le_abs _) cv). - rewrite Qplus_comm. - setoid_replace (1#p)%Q with (2 # 2*p)%Q. rewrite Qinv_minus_distr. - reflexivity. reflexivity. -Qed. - -Lemma CReal_absSmall : forall (x y : CReal) (n : positive), - (Qlt (2 # n) - (proj1_sig x (Pos.to_nat n) - Qabs (proj1_sig y (Pos.to_nat n)))) - -> CReal_abs y <= x. -Proof. - intros x y n maj. apply CReal_abs_le. split. - - apply CRealLt_asym. exists n. destruct x as [xn caux], y as [yn cauy]; simpl. - simpl in maj. unfold Qminus. rewrite Qopp_involutive. - rewrite Qplus_comm. - apply (Qlt_le_trans _ (xn (Pos.to_nat n) - Qabs (yn (Pos.to_nat n)))). - apply maj. apply Qplus_le_r. - rewrite <- (Qopp_involutive (yn (Pos.to_nat n))). - apply Qopp_le_compat. rewrite Qabs_opp. apply Qle_Qabs. - - apply CRealLt_asym. exists n. destruct x as [xn caux], y as [yn cauy]; simpl. - simpl in maj. - apply (Qlt_le_trans _ (xn (Pos.to_nat n) - Qabs (yn (Pos.to_nat n)))). - apply maj. apply Qplus_le_r. apply Qopp_le_compat. apply Qle_Qabs. -Qed. - -(* An element of CReal is a Cauchy sequence of rational numbers, - show that it converges to itself in CReal. *) -Lemma CReal_cv_self : forall (qn : nat -> Q) (x : CReal) (cvmod : positive -> nat), - QSeqEquiv qn (fun n => proj1_sig x n) cvmod - -> seq_cv (fun n => inject_Q (qn n)) x. +(* For instance the rational sequence 1/n converges to 0. *) +Lemma CReal_cv_self : forall (x : CReal) (n : positive), + CReal_abs (x - inject_Q (proj1_sig x n)) <= inject_Q (1#n). Proof. - intros qn x cvmod H p. - specialize (H (2*p)%positive). exists (cvmod (2*p)%positive). - intros p0 H0. - apply (CReal_absSmall - _ _ (Pos.max (4 * p)%positive (Pos.of_nat (cvmod (2 * p)%positive)))). - setoid_replace (proj1_sig (inject_Q (1 # p)) (Pos.to_nat (Pos.max (4 * p) (Pos.of_nat (cvmod (2 * p)%positive))))) - with (1 # p)%Q. - 2: reflexivity. - setoid_replace (proj1_sig (CReal_plus (inject_Q (qn p0)) (CReal_opp x)) (Pos.to_nat (Pos.max (4 * p) (Pos.of_nat (cvmod (2 * p)%positive))))) - with (qn p0 - proj1_sig x (2 * (Pos.to_nat (Pos.max (4 * p) (Pos.of_nat (cvmod (2 * p)%positive)))))%nat)%Q. - 2: destruct x; reflexivity. - apply (Qle_lt_trans _ (1 # 2 * p)). - unfold Qle; simpl. rewrite Pos2Z.inj_max. apply Z.le_max_l. - rewrite <- (Qplus_lt_r - _ _ (Qabs - (qn p0 - - proj1_sig x - (2 * Pos.to_nat (Pos.max (4 * p) (Pos.of_nat (cvmod (2 * p)%positive))))%nat) - -(1#2*p))). - ring_simplify. - setoid_replace (-1 * (1 # 2 * p) + (1 # p))%Q with (1 # 2 * p)%Q. - apply H. apply H0. rewrite Pos2Nat.inj_max. - apply (le_trans _ (1 * Nat.max (Pos.to_nat (4 * p)) (Pos.to_nat (Pos.of_nat (cvmod (2 * p)%positive))))). - destruct (cvmod (2*p)%positive). apply le_0_n. rewrite mult_1_l. - rewrite Nat2Pos.id. 2: discriminate. apply Nat.le_max_r. - apply Nat.mul_le_mono_nonneg_r. apply le_0_n. auto. - setoid_replace (1 # p)%Q with (2 # 2 * p)%Q. - rewrite Qplus_comm. rewrite Qinv_minus_distr. - reflexivity. reflexivity. + intros x n [k kmaj]. + destruct x as [xn cau]. + unfold CReal_abs, CReal_minus, CReal_plus, CReal_opp, inject_Q, proj1_sig in kmaj. + apply (Qlt_not_le _ _ kmaj). clear kmaj. + unfold QCauchySeq, QSeqEquiv in cau. + rewrite <- (Qplus_le_l _ _ (1#n)). ring_simplify. unfold id in cau. + destruct (Pos.lt_total (2*k) n). 2: destruct H. + - specialize (cau k (2*k)%positive n). + assert (k <= 2 * k)%positive. + { apply (Pos.le_trans _ (1*k)). apply Pos.le_refl. + apply Pos.mul_le_mono_r. discriminate. } + apply (Qle_trans _ (1#k)). apply Qlt_le_weak, cau. + exact H0. apply (Pos.le_trans _ _ _ H0). apply Pos.lt_le_incl, H. + rewrite <- (Qinv_plus_distr 1 1). + apply (Qplus_le_l _ _ (-(1#k))). ring_simplify. discriminate. + - subst n. rewrite Qplus_opp_r. discriminate. + - specialize (cau n (2*k)%positive n). + apply (Qle_trans _ (1#n)). apply Qlt_le_weak, cau. + apply Pos.lt_le_incl, H. apply Pos.le_refl. + apply (Qplus_le_l _ _ (-(1#n))). ring_simplify. discriminate. Qed. -(* Q is dense in Archimedean fields, so all real numbers - are limits of rational sequences. - The biggest computable such field has all rational limits. *) -Lemma R_has_all_rational_limits : forall qn : nat -> Q, - Un_cauchy_Q qn - -> { r : CReal & seq_cv (fun n:nat => inject_Q (qn n)) r }. +(* We can probably reduce the factor 4. *) +Lemma Rcauchy_limit : forall (xn : nat -> CReal) (xcau : Un_cauchy_mod xn), + QCauchySeq + (fun n : positive => + let (p, _) := xcau (4 * n)%positive in proj1_sig (xn p) (4 * n)%positive) id. Proof. - (* qn is an element of CReal. Show that inject_Q qn - converges to it in CReal. *) - intros. - destruct (standard_modulus qn (fun p => proj1_sig (H (Pos.succ p)))). - - intros p n k H0 H1. destruct (H (Pos.succ p)%positive) as [x a]; simpl in H0,H1. - specialize (a n k H0 H1). - apply (Qle_lt_trans _ (1#Pos.succ p) _ a). - apply Pos2Z.pos_lt_pos. simpl. apply Pos.lt_succ_diag_r. - - exists (exist _ (fun n : nat => - qn (increasing_modulus (fun p : positive => proj1_sig (H (Pos.succ p))) n)) H0). - apply (CReal_cv_self qn (exist _ (fun n : nat => - qn (increasing_modulus (fun p : positive => proj1_sig (H (Pos.succ p))) n)) H0) - (fun p : positive => Init.Nat.max (proj1_sig (H (Pos.succ p))) (Pos.to_nat p))). - apply H1. + intros xn xcau n p q H0 H1. + destruct (xcau (4 * p)%positive) as [i imaj], + (xcau (4 * q)%positive) as [j jmaj]. + assert (CReal_abs (xn i - xn j) <= inject_Q (1 # 4 * n)). + { destruct (le_lt_dec i j). + apply (CReal_le_trans _ _ _ (imaj i j (le_refl _) l)). + apply inject_Q_le. unfold Qle, Qnum, Qden. + rewrite Z.mul_1_l, Z.mul_1_l. apply Pos2Z.pos_le_pos. + apply Pos.mul_le_mono_l, H0. apply le_S, le_S_n in l. + apply (CReal_le_trans _ _ _ (jmaj i j l (le_refl _))). + apply inject_Q_le. unfold Qle, Qnum, Qden. + rewrite Z.mul_1_l, Z.mul_1_l. apply Pos2Z.pos_le_pos. + apply Pos.mul_le_mono_l, H1. } + clear jmaj imaj. + setoid_replace (1#n)%Q with ((1#(3*n)) + ((1#(3*n)) + (1#(3*n))))%Q. + 2: rewrite Qinv_plus_distr, Qinv_plus_distr; reflexivity. + apply lt_inject_Q. rewrite inject_Q_plus. + rewrite Qabs_Rabs. + apply (CReal_le_lt_trans _ (CReal_abs (inject_Q (proj1_sig (xn i) (4 * p)%positive) - xn i) + CReal_abs (xn i - inject_Q(proj1_sig (xn j) (4 * q)%positive)))). + unfold Qminus. + rewrite inject_Q_plus, opp_inject_Q. + setoid_replace (inject_Q (proj1_sig (xn i) (4 * p)%positive) + + - inject_Q (proj1_sig (xn j) (4 * q)%positive)) + with (inject_Q (proj1_sig (xn i) (4 * p)%positive) - xn i + + (xn i - inject_Q (proj1_sig (xn j) (4 * q)%positive))). + 2: ring. + apply CReal_abs_triang. apply CReal_plus_le_lt_compat. + rewrite CReal_abs_minus_sym. apply (CReal_le_trans _ (inject_Q (1# 4*p))). + apply CReal_cv_self. apply inject_Q_le. unfold Qle, Qnum, Qden. + rewrite Z.mul_1_l, Z.mul_1_l. + apply Pos2Z.pos_le_pos. apply (Pos.le_trans _ (4*n)). + apply Pos.mul_le_mono_r. discriminate. + apply Pos.mul_le_mono_l. exact H0. + apply (CReal_le_lt_trans + _ (CReal_abs (xn i - xn j + (xn j - inject_Q (proj1_sig (xn j) (4 * q)%positive))))). + apply CReal_abs_morph. ring. + apply (CReal_le_lt_trans _ _ _ (CReal_abs_triang _ _)). + rewrite inject_Q_plus. apply CReal_plus_le_lt_compat. + apply (CReal_le_trans _ _ _ H). apply inject_Q_le. + unfold Qle, Qnum, Qden. rewrite Z.mul_1_l, Z.mul_1_l. + apply Pos2Z.pos_le_pos. apply Pos.mul_le_mono_r. discriminate. + apply (CReal_le_lt_trans _ (inject_Q (1#4*q))). + apply CReal_cv_self. apply inject_Q_lt. unfold Qlt, Qnum, Qden. + rewrite Z.mul_1_l, Z.mul_1_l. + apply Pos2Z.pos_lt_pos. apply (Pos.lt_le_trans _ (4*n)). + apply Pos.mul_lt_mono_r. reflexivity. + apply Pos.mul_le_mono_l. exact H1. Qed. Lemma Rcauchy_complete : forall (xn : nat -> CReal), @@ -350,49 +216,63 @@ Lemma Rcauchy_complete : forall (xn : nat -> CReal), -> { l : CReal & seq_cv xn l }. Proof. intros xn cau. - destruct (R_has_all_rational_limits (fun n => let (l,_) := RQ_limit (xn n) n in l) - (Rdiag_cauchy_sequence xn cau)) - as [l cv]. - exists l. intro p. specialize (cv (2*p)%positive) as [k cv]. - exists (max k (2 * Pos.to_nat p)). intros p0 H. - specialize (cv p0 (le_trans _ _ _ (Nat.le_max_l _ _) H)). - destruct (RQ_limit (xn p0) p0) as [q maj]. - apply CReal_abs_le. split. - - apply (CReal_le_trans _ (inject_Q q - inject_Q (1 # 2 * p) - l)). - + unfold CReal_minus. rewrite (CReal_plus_comm (inject_Q q)). - apply (CReal_plus_le_reg_r (inject_Q (1 # p) + l - inject_Q q)). - ring_simplify. unfold CReal_minus. - rewrite <- (opp_inject_Q (1# 2*p)), <- inject_Q_plus. - setoid_replace ((1 # p) + - (1 # 2* p))%Q with (1#2*p)%Q. - rewrite CReal_abs_minus_sym in cv. - exact (CReal_le_trans _ _ _ (CReal_le_abs _) cv). - setoid_replace (1#p)%Q with (2 # 2*p)%Q. - rewrite Qinv_minus_distr. reflexivity. reflexivity. - + unfold CReal_minus. - do 2 rewrite <- (CReal_plus_comm (-l)). apply CReal_plus_le_compat_l. - apply (CReal_plus_le_reg_r (inject_Q (1 # 2 * p))). - ring_simplify. rewrite CReal_plus_comm. - apply (CReal_le_trans _ (xn p0 + inject_Q (1 # Pos.of_nat p0))). - apply CRealLt_asym, maj. apply CReal_plus_le_compat_l. - apply inject_Q_le. - apply Z2Nat.inj_le. discriminate. discriminate. - simpl. assert ((Pos.to_nat p~0 <= p0)%nat). - { apply (le_trans _ (Init.Nat.max k (2 * Pos.to_nat p))). - 2: apply H. replace (p~0)%positive with (2*p)%positive. - 2: reflexivity. rewrite Pos2Nat.inj_mul. - apply Nat.le_max_r. } - rewrite Nat2Pos.id. apply H0. intro abs. subst p0. - inversion H0. pose proof (Pos2Nat.is_pos (p~0)). - rewrite H2 in H1. inversion H1. - - apply (CReal_le_trans _ (inject_Q q - l)). - + unfold CReal_minus. do 2 rewrite <- (CReal_plus_comm (-l)). - apply CReal_plus_le_compat_l. apply CRealLt_asym, maj. - + apply (CReal_le_trans _ (inject_Q (1 # 2 * p))). - exact (CReal_le_trans _ _ _ (CReal_le_abs _) cv). - apply inject_Q_le. rewrite <- Qplus_0_r. - setoid_replace (1#p)%Q with ((1#2*p)+(1#2*p))%Q. - apply Qplus_le_r. discriminate. - rewrite Qinv_plus_distr. reflexivity. + exists (exist _ (fun n : positive => + let (p, _) := cau (4 * n)%positive in + proj1_sig (xn p) (4 * n)%positive) + (Rcauchy_limit xn cau)). + intro p. + pose proof (CReal_cv_self (exist _ (fun n : positive => + let (p, _) := cau (4 * n)%positive in + proj1_sig (xn p) (4 * n)%positive) + (Rcauchy_limit xn cau)) (2*p)) as H. + simpl (inject_Q + (proj1_sig + (exist (fun x : positive -> Q => QCauchySeq x id) + (fun n : positive => + let (p, _) := cau (4 * n)%positive in + proj1_sig (xn p) (4 * n)%positive) (Rcauchy_limit xn cau)) + (2 * p)%positive)) in H. + pose proof (cau (2*p)%positive) as [k cv]. + destruct (cau (p~0~0~0)%positive) as [i imaj]. + (* The convergence modulus does not matter here, because a converging Cauchy + sequence always converges to its limit with twice the Cauchy modulus. *) + exists (max k i). + intros j H0. + setoid_replace (xn j - + exist (fun x : positive -> Q => QCauchySeq x id) + (fun n : positive => + let (p0, _) := cau (4 * n)%positive in proj1_sig (xn p0) (4 * n)%positive) + (Rcauchy_limit xn cau)) + with (xn j - inject_Q (proj1_sig (xn i) (p~0~0~0)%positive) + + (inject_Q (proj1_sig (xn i) (p~0~0~0)%positive) - + exist (fun x : positive -> Q => QCauchySeq x id) + (fun n : positive => + let (p0, _) := cau (4 * n)%positive in proj1_sig (xn p0) (4 * n)%positive) + (Rcauchy_limit xn cau))). + 2: ring. apply (CReal_le_trans _ _ _ (CReal_abs_triang _ _)). + apply (CReal_le_trans _ (inject_Q (1#2*p) + inject_Q (1#2*p))). + apply CReal_plus_le_compat. + 2: rewrite CReal_abs_minus_sym; exact H. + specialize (imaj j i (le_trans _ _ _ (Nat.le_max_r _ _) H0) (le_refl _)). + apply (CReal_le_trans _ (inject_Q (1 # 4 * p) + inject_Q (1 # 4 * p))). + setoid_replace (xn j - inject_Q (proj1_sig (xn i) (p~0~0~0)%positive)) + with (xn j - xn i + + (xn i - inject_Q (proj1_sig (xn i) (p~0~0~0)%positive))). + 2: ring. apply (CReal_le_trans _ _ _ (CReal_abs_triang _ _)). + apply CReal_plus_le_compat. apply (CReal_le_trans _ _ _ imaj). + apply inject_Q_le. unfold Qle, Qnum, Qden. + rewrite Z.mul_1_l, Z.mul_1_l. + apply Pos2Z.pos_le_pos. + apply (Pos.mul_le_mono_r p 4 8). discriminate. + apply (CReal_le_trans _ _ _ (CReal_cv_self (xn i) (8*p))). + apply inject_Q_le. unfold Qle, Qnum, Qden. + rewrite Z.mul_1_l, Z.mul_1_l. + apply Pos2Z.pos_le_pos. + apply (Pos.mul_le_mono_r p 4 8). discriminate. + rewrite <- inject_Q_plus. rewrite (inject_Q_morph _ (1#2*p)). + apply CRealLe_refl. rewrite Qinv_plus_distr; reflexivity. + rewrite <- inject_Q_plus. rewrite (inject_Q_morph _ (1#p)). + apply CRealLe_refl. rewrite Qinv_plus_distr; reflexivity. Qed. Lemma CRealLtIsLinear : isLinearOrder CRealLt. |