proposition: Lemma CRln_pos_ln : forall (c:Qpos) (x:CR) Hx, ('proj1_sig c <= x -> CRln_pos c x == CRln x Hx)%CR.
proof: Proof. intros c x Hx Hc. assert (X:[0][<](CRasIR x)). apply CR_less_as_IR. apply CRltT_wd with 0%CR x; try assumption. rewrite -> IR_Zero_as_CR. reflexivity. rewrite -> CRasIRasCR_id. reflexivity. destruct Hx as [d Hd]. unfold CRln. rewrite <- (CRasIRasCR_id x). rewrite <- (CRln_pos_correct c _ X). rewrite <- (CRln_pos_correct d _ X). reflexivity. change (inj_Q IR (proj1_sig d)[<=](CRasIR x)). rewrite -> IR_leEq_as_CR. autorewrite with IRtoCR. rewrite -> CRasIRasCR_id. ring_simplify in Hd. assumption. change (inj_Q IR (proj1_sig c)[<=](CRasIR x)). rewrite -> IR_leEq_as_CR. autorewrite with IRtoCR. rewrite -> CRasIRasCR_id. assumption. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.reals.fast.CRartanh_slow CoRN.reals.fast.CRArith CoRN.reals.fast.CRIR Coq.QArith.Qpower CoRN.model.ordfields.Qordfield CoRN.reals.fast.ModulusDerivative CoRN.reals.fast.ContinuousCorrect CoRN.model.metric2.Qmetric CoRN.tactics.Qauto CoRN.transc.Exponential CoRN.transc.ArTanH CoRN.tactics.CornTac