proposition: Lemma arctanStream_zl : Limit_zero _ arctanStream (xH,a) (fun e:Qpos => Z.to_pos (Qceiling (/ (proj1_sig e)))).
proof: Proof. intros [e epos]. rewrite Str_pth_arctanStream, Qabs_Qmult, Qabs_Qmult. rewrite Qabs_Qpower. change (Qabs (-1)) with 1. rewrite Qpower_1, Qmult_1_l. rewrite Qmult_comm. apply (Qle_trans _ (1 * Qabs (1 # 1 + 2 * Z.to_pos (Qceiling (/ ` (e ↾ epos)))))). apply Qmult_le_compat_r. 2: apply Qabs_nonneg. - rewrite (Qabs_Qpower a (1 + 2 * Z.to_pos (Qceiling (/ ` (e ↾ epos))))). apply Qpower_le_1. split. apply Qabs_nonneg. apply Qabs_Qle_condition, Ha. - clear Ha a. rewrite Qmult_1_l. unfold Qabs, Z.abs, proj1_sig. rewrite <- (Qinv_involutive e) at 2. assert (0 < /e) as H. { apply Qinv_lt_0_compat, epos. } apply (@Qinv_le_compat (/e) (Zpos (1 + 2 * Z.to_pos (Qceiling (/ e))) # 1)). exact H. apply (Qle_trans _ _ _ (Qle_ceiling (/e))). generalize (Qceiling (/ e)). clear H epos e. intros [|p|p]. discriminate. 2: discriminate. pose proof (Zle_Qle p (Z.pos (1 + 2 * Z.to_pos p))). unfold inject_Z. unfold inject_Z in H. rewrite <- H. clear H. change (p <= 1 + 2*p)%positive. rewrite <- Pplus_one_succ_l. apply Pos.lt_le_incl, Pos.lt_succ_r. apply (Pos.mul_le_mono_r p 1 2). discriminate. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.reals.fast.CRAlternatingSum CoRN.reals.fast.CRAlternatingSum_alg CoRN.reals.fast.CRstreams CoRN.reals.fast.CRexp CoRN.reals.fast.CRArith CoRN.reals.fast.CRIR Coq.QArith.Qpower Coq.QArith.Qabs Coq.QArith.Qround CoRN.model.ordfields.Qordfield CoRN.reals.Q_in_CReals CoRN.model.metric2.Qmetric CoRN.model.totalorder.QMinMax CoRN.model.totalorder.QposMinMax CoRN.transc.MoreArcTan CoRN.tactics.CornTac MathClasses.interfaces.abstract_algebra CoRN.stdlib_omissions.Q Coq.Init.Datatypes