proposition: Lemma artanh_DomArTanH : forall a, (a^2 < 1) -> DomArTanH (inj_Q IR a).
proof: Proof. intros a Ha. split. stepl (inj_Q IR (-(1))%Q). apply inj_Q_less; simpl. apply Qnot_le_lt. intros H. apply (Qlt_not_le _ _ Ha). rewrite -> Qle_minus_iff in *. replace RHS with ((- (1) + - a + 2)*(-(1) +- a)) by simpl; ring. Qauto_nonneg. stepr ([--](inj_Q IR 1)). apply inj_Q_inv. apply un_op_wd_unfolded. rstepr (nring 1:IR). apply (inj_Q_nring IR 1). stepr (inj_Q IR (1)). apply inj_Q_less; simpl. apply Qnot_le_lt. intros H. apply (Qlt_not_le _ _ Ha). rewrite -> Qle_minus_iff in *. replace RHS with ((a + - (1) + 2)*(a +- (1))) by simpl; ring. Qauto_nonneg. rstepr (nring 1:IR). apply (inj_Q_nring IR 1). Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.reals.iso_CReals CoRN.reals.fast.CRAlternatingSum CoRN.reals.fast.CRGeometricSum CoRN.reals.fast.CRstreams CoRN.reals.fast.CRArith CoRN.reals.fast.CRIR Coq.QArith.Qabs Coq.QArith.Qpower CoRN.model.ordfields.Qordfield CoRN.reals.Q_in_CReals CoRN.model.metric2.Qmetric CoRN.model.totalorder.QMinMax CoRN.transc.ArTanH CoRN.reals.fast.CRarctan_small CoRN.tactics.Qauto CoRN.tactics.CornTac