proposition: Lemma ln2_correct : (ln2 == IRasCR (Log Two (pos_two IR)))%CR.
proof: Proof. unfold ln2. rewrite -> rational_ln_slow_correct'. apply IRasCR_wd. apply Log_wd. apply (inj_Q_nring IR 2). 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