proposition: Lemma lnDomainAdaptor : forall a, (0 < a) -> (let (n,d) := a in (n - Zpos d)/(n + Zpos d))^2 < 1.
proof: Proof. intros [[|n|n] d] Ha; try solve [elim (Qlt_not_le _ _ Ha); auto with *]. simpl. replace LHS with ((n-d)*(n-d)/((n+d)*(n+d))) by simpl; field; auto with *. apply Qlt_shift_div_r. auto with *. rewrite -> Qlt_minus_iff. ring_simplify. Qauto_pos. 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