proposition: Lemma app_inverse_below_correct : forall q:Qpos, AQtoQ (app_inverse_below q) <= proj1_sig q.
proof: Proof. intros. unfold app_inverse_below. destruct aq_dense_embedding. specialize (dense_inverse ((3 # 4) * ` q)%Q ((1#4)*q)%Qpos). apply AbsSmall_Qabs, Qabs_Qle_condition in dense_inverse. destruct dense_inverse as [_ H5]. simpl in H5. apply (Qplus_le_r _ _ ((3 # 4) * ` q)) in H5. ring_simplify in H5. exact H5. Qed.
imports: Coq.QArith.Qabs CoRN.util.Qdlog CoRN.algebra.RSetoid CoRN.model.totalorder.QposMinMax CoRN.model.metric2.Qmetric CoRN.model.reals.CRreal CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.reals.fast.CRAlternatingSum CoRN.reals.fast.CRstreams CoRN.reals.faster.ApproximateRationals CoRN.reals.faster.ARArith