proposition: Lemma rational_ln_correct : forall (a:Q) Ha Ha0, (@rational_ln a Ha == IRasCR (Log (inj_Q IR a) Ha0))%CR.
proof: Proof. intros a Ha Ha0. unfold rational_ln. rewrite <- ln_scale_by_two_power. do 2 rewrite <- CRmult_scale. change (((- ln_scale_power_factor Ha)%Z):Q) with ((- ln_scale_power_factor Ha)%Q). rewrite <- CRopp_Qopp. ring_simplify. apply rational_ln_slow_correct. 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