proposition: Lemma CRln_pos_correct : forall (c:Qpos) x Hx, closel (inj_Q _ (proj1_sig c)) x -> (IRasCR (Log x Hx)==CRln_pos c (IRasCR x))%CR.
proof: Proof. intros c x Hx Hx0. assert (Z:Continuous (closel (inj_Q IR (proj1_sig c))) Logarithm). apply (Included_imp_Continuous (openl [0])). Contin. clear - c. intros x Hx. simpl. apply less_leEq_trans with (inj_Q IR (proj1_sig c)); try assumption. stepl (inj_Q IR 0). apply inj_Q_less. simpl; auto with *. apply (inj_Q_nring IR 0). apply (fun x => @ContinuousCorrect _ x Logarithm Z); auto with *. constructor. intros q Hq H. change (CRln_pos c (' q) == IRasCR (Log (inj_Q IR q) Hq))%CR. transitivity (ln_pos_uc c q);[|]. unfold CRln_pos. change (' q)%CR with (Cunit_fun Q_as_MetricSpace q). pose proof (Cbind_correct QPrelengthSpace (ln_pos_uc c)). apply ucEq_equiv in H0. rewrite -> (H0 (Cunit_fun Q_as_MetricSpace q)). apply BindLaw1. simpl. rewrite -> rational_ln_correct'. apply IRasCR_wd. apply Log_wd. apply inj_Q_wd. simpl. rewrite <- Qle_max_r. apply leEq_inj_Q with IR. 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