proposition: Lemma CRmult_inv_r_pos : forall (x : CR) (xnz : (x >< 0)%CR), (0 < x)%CR -> (x * CRinvT x xnz == 1).
proof: Proof. intros. destruct xnz. exfalso. exact (CRlt_irrefl x (CRlt_trans _ _ _ c H)). destruct c as [q pos]. unfold CRinvT. rewrite CRopp_0, CRplus_0_r in pos. pose (Qpos_max (Qpos_inv q) (CR_b (1#1) x + (1#1))) as b. assert (' (- ` b)%Q <= x) as xlower. { apply (@CRle_trans _ (' (-proj1_sig (CR_b (1#1) x))%Q)). 2: apply (CR_b_lowerBound _ _). apply CRle_Qle. apply Qopp_le_compat. apply (Qle_trans _ (proj1_sig (CR_b (1#1)%Qpos x) + (1#1))). rewrite <- Qplus_0_r at 1. apply Qplus_le_r. discriminate. apply (Qpos_max_ub_r (Qpos_inv q) (CR_b (1#1) x + (1#1))). } assert (x <= '(` b)%Q) as xupper. { apply (@CRle_trans _ (' (proj1_sig (CR_b (1#1) x))) _ (CR_b_upperBound _ _)). apply CRle_Qle. apply (Qle_trans _ (proj1_sig (CR_b (1#1)%Qpos x) + (1#1))). rewrite <- Qplus_0_r at 1. apply Qplus_le_r. discriminate. apply (Qpos_max_ub_r (Qpos_inv q) (CR_b (1#1) x + (1#1))). } rewrite <- (CRboundAbs_Eq _ xlower xupper). assert (`q < `b)%Q as qltb. { apply Qlt_from_CRlt. apply (CRle_lt_trans _ _ _ pos). apply (CRle_lt_trans _ _ _ (CR_b_upperBound (1#1) x)). apply CRlt_Qlt. unfold b. apply (Qlt_le_trans _ (proj1_sig (CR_b (1#1) x + (1#1))%Qpos)). rewrite <- Qplus_0_r. apply Qplus_lt_r. reflexivity. apply Qpos_max_ub_r. } assert (/`q <= `b)%Q as invqleb. { apply (Qpos_max_ub_l (Qpos_inv q) (CR_b (1#1) x + (1#1))). } rewrite <- (CRmult_bounded_mult b). apply (CRmult_inv_r_bounded (CRboundAbs b x) q b). - rewrite (CRboundAbs_Eq _ xlower xupper). exact pos. - exact qltb. - exact invqleb. - intros. simpl. apply Qmax_lub. apply (Qle_trans _ 0). apply (Qopp_le_compat 0), Qpos_nonneg. apply Qpos_nonneg. apply Qmin_lb_l. - intros. simpl. apply Qmax_ub_l. - rewrite (CRboundAbs_Eq _ xlower xupper). intro e. simpl. unfold Cap_raw. simpl. rewrite Qopp_involutive. apply (Qle_trans _ 0). apply (Qopp_le_compat 0), Qpos_nonneg. apply (Qle_trans _ (/ Qmax (` q) (approximate x (Qinv_modulus q ((1 # 2) ↾ eq_refl * e))) + 0)). rewrite Qplus_0_r. apply Qlt_le_weak, Qinv_lt_0_compat. apply (Qlt_le_trans _ (`q)). apply Qpos_ispos. apply Qmax_ub_l. apply Qplus_le_r. apply Qpos_nonneg. - rewrite (CRboundAbs_Eq _ xlower xupper). intro e. simpl. unfold Cap_raw. simpl. apply (Qle_trans _ 0). apply (Qopp_le_compat 0), Qpos_nonneg. rewrite <- Qle_minus_iff. apply (Qle_trans _ (/ `q)). 2: apply (Qpos_max_ub_l (Qpos_inv q) (CR_b (1#1) x + (1#1))). apply Qle_shift_inv_r. apply (Qlt_le_trans _ (`q)). apply Qpos_ispos. apply Qmax_ub_l. rewrite Qmult_comm. apply Qle_shift_div_l. apply Qpos_ispos. rewrite Qmult_1_l. apply Qmax_ub_l. 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