proposition: Lemma CRinv_pos_weaken : forall (c1 c2:Qpos), proj1_sig c1 <= proj1_sig c2 -> forall (x:CR), (' proj1_sig c2 <= x -> CRinv_pos c1 x == CRinv_pos c2 x)%CR.
proof: Proof. intros c1 c2 Hc x Hx. assert (X:((boundBelow (proj1_sig c2) x)==x)%CR). rewrite <- CRmax_boundBelow. rewrite <- CRle_max_r. assumption. rewrite <- X. rewrite <- (QreduceApprox_Eq x). pose (f:=(fun e:Qpos => (c1*c1*Qpos_inv c2*Qpos_inv c2)*e)%Qpos). assert (Y:forall e:Qpos, proj1_sig (f e) <= proj1_sig e). { intros e. unfold f. simpl. rewrite <- (Qmult_1_l (`e)) at 2. apply Qmult_le_r. apply Qpos_ispos. apply Qle_shift_div_r. apply Qpos_ispos. apply Qle_shift_div_r. apply Qpos_ispos. rewrite Qmult_1_l. apply (Qle_trans _ (`c1*`c2)). apply Qmult_le_l. apply Qpos_ispos. exact Hc. apply Qmult_le_r. apply Qpos_ispos. exact Hc. } transitivity (CRinv_pos c2 (boundBelow (proj1_sig c2) (faster (QreduceApprox x) f Y))). apply regFunEq_equiv, regFunEq_e. intros e. assert (Z:=Qinv_pos_uc_wd _ _ Hc). simpl in Z. simpl. rewrite -> Z;[|apply Qmax_ub_l]. unfold Qinv_modulus. replace (Qpos_red (c1 * c1 * e)) with (Qpos_red (f (c2 * c2 * e)%Qpos)); [apply ball_refl|]. apply (Qpos_nonneg (e+e)). apply Qpos_red_eq. unfold f. unfold QposEq. simpl. field. apply Qpos_nonzero. rewrite -> fasterIsEq. reflexivity. Qed.
imports: CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QposMinMax CoRN.model.lattice.CRlattice CoRN.model.totalorder.QMinMax Coq.QArith.Qabs CoRN.model.metric2.Qmetric CoRN.metric2.ProductMetric MathClasses.interfaces.canonical_names