proposition: Lemma CRinv_0_lt_compat : forall (x : CR) (xnz : (x >< 0)%CR), (0 < x -> 0 < CRinvT x xnz)%CR.
proof: Proof. intros. unfold CRinvT. destruct xnz. - exfalso. apply (CRlt_irrefl x). exact (CRlt_trans _ _ _ c H). - destruct c as [q c]. pose (CR_b (1#1) x + (1#1))%Qpos as b. exists (Qpos_inv b). rewrite CRopp_0, CRplus_0_r. rewrite CRopp_0, CRplus_0_r in c. intro e. simpl. unfold Cap_raw. simpl. unfold Qinv_modulus. change (Qabs (approximate x (Qpos2QposInf (1 # 1))) + 1 + 1)%Q with (`b). assert (`q <= `b)%Q as qleb. { apply CRle_Qle. apply (CRle_trans c). apply (CRle_trans (CR_b_upperBound (1#1)%Qpos x)). simpl. apply CRle_Qle. rewrite <- Qplus_assoc. apply Qplus_le_r. discriminate. } apply Qmax_case. + intros _. apply (Qle_trans _ 0). apply (Qopp_le_compat 0), Qpos_nonneg. rewrite <- Qle_minus_iff. apply Qle_shift_inv_r. apply Qpos_ispos. rewrite Qmult_comm. apply Qle_shift_div_l. apply Qpos_ispos. rewrite Qmult_1_l. exact qleb. + intros. apply (Qmult_le_l _ _ (approximate x (q * q * ((1 # 2)%Q ↾ eq_refl * e))%Qpos)). exact (Qlt_le_trans _ (`q) _ (Qpos_ispos q) H0). rewrite Qmult_plus_distr_r, Qmult_inv_r. apply (Qmult_le_l _ _ (`b)). apply Qpos_ispos. rewrite Qmult_plus_distr_r. setoid_replace (` b * ((approximate x (q * q * ((1 # 2) * e))%Qpos) * - / ` b))%Q with (-(approximate x (q * q * ((1 # 2)%Q ↾ eq_refl * e))%Qpos))%Q by (unfold equiv, stdlib_rationals.Q_eq; field). 2: apply Qpos_nonzero. rewrite Qmult_1_r. apply (Qle_trans _ (-(`q * `q * `e))). setoid_replace (` b * (approximate x (q * q * ((1 # 2)%Q ↾ eq_refl * e))%Qpos * - ` e))%Q with (-(` b * (approximate x (q * q * ((1 # 2)%Q ↾ eq_refl * e))%Qpos *` e)))%Q by (unfold equiv, stdlib_rationals.Q_eq; ring). apply Qopp_le_compat. rewrite Qmult_assoc. apply Qmult_le_r. apply Qpos_ispos. apply Qpos_mult_le_compat. exact qleb. exact H0. unfold b, CR_b. simpl. rewrite <- (Qabs_pos (approximate x (q * q * ((1 # 2)%Q ↾ eq_refl * e))%Qpos)). apply (Qle_trans _ (-((1#1)+(`q * `q * ((1 # 2) * `e))) + (2#1)))%Q. apply (Qle_trans _ (-(`q * `q * ((1 # 2) * `e)))). apply Qopp_le_compat. apply Qmult_le_l. apply (Qpos_ispos (q*q)). rewrite <- (Qmult_1_l (`e)) at 2. apply Qmult_le_r. apply Qpos_ispos. discriminate. rewrite <- Qplus_0_r. setoid_replace (- ((1#1) + ` q * ` q * ((1 # 2) * ` e)) + (2#1))%Q with (- (` q * ` q * ((1 # 2) * ` e)) + (1#1))%Q by (unfold equiv, stdlib_rationals.Q_eq; ring). apply Qplus_le_r. discriminate. rewrite <- Qplus_assoc, <- Qplus_assoc, (Qplus_assoc (1#1)). setoid_replace ((1#1)+(1#1))%Q with (2#1)%Q by reflexivity. rewrite (Qplus_comm (2#1)), Qplus_assoc. apply Qplus_le_compat. apply (reverseRegFun x (1#1) (q * q * ((1 # 2) * e))). discriminate. apply (Qle_trans _ (`q)). apply Qpos_nonneg. exact H0. intro abs. rewrite abs in H0. apply (Qle_not_lt _ _ H0), Qpos_ispos. Qed.
imports: CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QMinMax CoRN.model.totalorder.QposMinMax Coq.setoid_ring.Ring_theory Coq.Setoids.Setoid Coq.QArith.QArith Coq.QArith.Qabs Coq.QArith.Qround CoRN.metric2.Complete CoRN.metric2.ProductMetric CoRN.reals.fast.CRFieldOps CoRN.model.metric2.Qmetric CoRN.logic.Stability Coq.Logic.ConstructiveEpsilon CoRN.util.Qdlog MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders