proposition: Lemma app_inverse_below_pos : forall q:Qpos, 0 < app_inverse_below 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. destruct aq_strict_order_embed. apply strict_order_embedding_reflecting. refine (Qlt_le_trans _ ((8 # 16) * ` q) _ _ H5). rewrite rings.preserves_0. apply (Qpos_ispos ((8#16)*q)). 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