proposition: Lemma CReal_inv_pos_cauchy: forall (x : CReal) (xPos : 0 < x), QCauchySeq (CReal_inv_pos_seq x xPos).
proof: Proof. intros x Hxpos n p q Hp Hq; unfold CReal_inv_pos_seq. unfold CReal_inv_pos_cm; remember (CRealLowerBound x Hxpos) as k. assert (forall m:Z, (2^k < seq x (Z.min k (m + 2 * k))))%Q as AuxAppart. { intros m. pose proof CRealLowerBoundSpec x Hxpos (Z.min k (m + 2 * k))%Z ltac:(lia) as H1. rewrite Heqk at 1. lra. } assert (forall m:Z, (0 < seq x (Z.min k (m + 2 * k))))%Q as AuxPos. { intros m. pose proof AuxAppart m as H1. pose proof Qpower_0_lt 2 k as H2. lra. } assert( forall a b : Q, (a>0)%Q -> (b>0)%Q -> (/a - /b == (b - a) / (a * b))%Q ) as H by (intros; field; lra); rewrite H by apply AuxPos; clear H. setoid_rewrite Qabs_Qmult; setoid_rewrite Qabs_Qinv. apply Qlt_shift_div_r. - setoid_rewrite <- (Qmult_0_l 0); setoid_rewrite Qabs_Qmult. apply Qmult_lt_compat_nonneg. 1,2: split; [lra | apply Qabs_gt, AuxPos]. - assert( forall r:Q, (r == (r/2^k/2^k)*(2^k*2^k))%Q ) as H by (intros r; field; apply Qpower_not_0; lra); rewrite H; clear H. apply Qmult_lt_compat_nonneg. + split. * do 2 (apply Qle_shift_div_l; [ apply Qpower_0_lt; lra | rewrite Qmult_0_l ]). apply Qabs_nonneg. * do 2 (apply Qlt_shift_div_r; [apply Qpower_0_lt; lra|]). do 2 rewrite <- Qpower_plus by lra. apply (cauchy x (n+k+k)%Z); lia. + split. * rewrite <- Qpower_plus by lra. apply Qpower_pos; lra. * setoid_rewrite Qabs_Qmult; apply Qmult_lt_compat_nonneg. 1,2: split; [apply Qpower_pos; lra | ]. 1,2: apply Qabs_gt, AuxAppart. Qed.
imports: QArith Qabs Qround Qpower Logic.ConstructiveEpsilon ConstructiveCauchyReals Lia Lqa QExtra