proposition: Lemma rational_arctan_small_correct : forall (a:Q) (Ha : -1 < a < 1), (@rational_arctan_small a (widen_interval Ha) == IRasCR (ArcTan (inj_Q IR a)))%CR.
proof: Proof. intros a Ha. unfold rational_arctan_small. rewrite <- (IR_inj_Q_as_CR a). rewrite (AltSeries_correct _ _ _ _ (arctanStream_alt (widen_interval Ha)) (arctanStream_zl (widen_interval Ha)) _ (AltSeries_convergent_0 _ _ _ _ (inj_Q IR a) (arctanStream_alt (widen_interval Ha)) (arctanStream_zl (widen_interval Ha)))). - apply IRasCR_wd. assert (olor ([--][1]) [1] (inj_Q IR a)) as X. { split. stepl (inj_Q IR (-1)). apply inj_Q_less, Ha. rewrite (inj_Q_inv IR 1), inj_Q_One. reflexivity. stepr (inj_Q IR 1); [| now apply inj_Q_One]. apply inj_Q_less, Ha. } eapply eq_transitive_unfolded; [|apply (arctan_series (inj_Q IR a) (arctan_series_convergent_IR) X)]. apply series_sum_wd. intros n. transitivity (inj_Q IR (((-1)^n)%Q *(a^(1+2*Z.of_nat n) * (1#(Pos.of_nat (1+2*n)))))). + destruct n. apply inj_Q_wd. simpl. rewrite Qmult_1_l, Qmult_1_r. reflexivity. apply inj_Q_wd. rewrite Str_pth_arctanStream. rewrite (Qmult_assoc ((-1)^S n)). rewrite (Qmult_comm ((-1) ^ S n * a ^ (1 + 2 * S n))). apply Qmult_comp. unfold Qeq, Qnum, Qden. rewrite Z.mul_1_l, Z.mul_1_l. change 2%positive with (Pos.of_nat 2). rewrite <- (Nat2Pos.inj_mul 2 (S n)). 2: discriminate. 2: discriminate. rewrite <- (Nat2Pos.inj_add 1). reflexivity. discriminate. discriminate. apply Qmult_comp. rewrite <- Pos.of_nat_succ, POS_anti_convert. reflexivity. replace (1 + 2 * Z.pos (Pos.of_nat (S n)))%Z with (1 + 2 * S n)%Z. reflexivity. rewrite <- Pos.of_nat_succ, POS_anti_convert. reflexivity. + transitivity (([--][1][^]n[/]nring (R:=IR) (S (2 * n))[//]nringS_ap_zero IR (2 * n))[*] (inj_Q IR a)[^](2 * n + 1)). 2: reflexivity. rstepr (([--][1][^]n)[*]((inj_Q IR a)[^](2*n+1)[/]nring (R:=IR) (S (2 * n))[//]nringS_ap_zero IR (2 * n))). rewrite inj_Q_mult. apply mult_wd. rewrite inj_Q_power. apply nexp_wd. rewrite (inj_Q_inv IR 1), inj_Q_One. reflexivity. apply mult_cancel_lft with (nring (R:=IR) (S (2 * n))). apply nringS_ap_zero. rstepr (inj_Q IR a[^](2 * n + 1)). stepr (inj_Q IR (a^(2*n+1)%nat)); [| now apply inj_Q_power]. stepl ((inj_Q IR (nring (S (2*n))))[*]inj_Q IR (a ^ (1 + 2 * n) * (1 # Pos.of_nat (1 + 2 * n)))); [| now apply mult_wdl; apply inj_Q_nring]. rewrite <- inj_Q_mult. apply inj_Q_wd. setoid_rewrite (nring_Q (S (2*n))). change (S (2 * n) * (a ^ (1 + 2 * n) * (1 # Pos.of_nat (1 + 2 * n))) == a ^ (2 * n + 1)%nat)%Q. rewrite Qmult_comm. rewrite <- Qmult_assoc. setoid_replace ((1 # Pos.of_nat (1 + 2 * n)) * S (2 * n)) with 1%Q. rewrite Qmult_1_r, Nat.add_comm. rewrite Nat2Z.inj_add, Nat2Z.inj_mul. reflexivity. unfold Qeq, inject_Z, Qmult, Qnum, Qden. rewrite Z.mul_1_l, Z.mul_1_l, Z.mul_1_r, Pos.mul_1_r. unfold Z.of_nat. rewrite Pos.of_nat_succ. reflexivity. - intro p. destruct (Pos.to_nat p) eqn:des. exfalso. pose proof (Pos2Nat.is_pos p). rewrite des in H. inversion H. apply inj_Q_wd. rewrite <- des, Pos2Nat.id. reflexivity. 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