proposition: Lemma CRln_wd : forall (x y:CR) Hx Hy, (x == y -> CRln x Hx == CRln y Hy)%CR.
proof: Proof. intros x y [c Hc] Hy Hxy. unfold CRln at 1. rewrite -> Hxy. apply CRln_pos_ln. rewrite <- Hxy. ring_simplify in Hc. 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