proposition: Lemma CRln_correct : forall x Hx Hx0, (IRasCR (Log x Hx)==CRln (IRasCR x) Hx0)%CR.
proof: Proof. intros x Hx [c Hc]. apply CRln_pos_correct. change ((inj_Q IR (proj1_sig c))[<=]x). rewrite -> IR_leEq_as_CR. rewrite -> IR_inj_Q_as_CR. setoid_replace (IRasCR x) with (IRasCR x - 0)%CR by (simpl; ring). 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