Library Coq.Reals.Machin

Require Import Lia.
Require Import Lra.
Require Import Rbase.
Require Import Rtrigo1.
Require Import Ranalysis_reg.
Require Import Rfunctions.
Require Import AltSeries.
Require Import Rseries.
Require Import SeqProp.
Require Import PartSum.
Require Import Ratan.

Local Open Scope R_scope.


Definition atan_sub u v := (u - v)/(1 + u * v).

Lemma atan_sub_correct :
 forall u v, 1 + u * v <> 0 -> -PI/2 < atan u - atan v < PI/2 ->
   -PI/2 < atan (atan_sub u v) < PI/2 ->
   atan u = atan v + atan (atan_sub u v).

Lemma tech : forall x y , -1 <= x <= 1 -> -1 < y < 1 ->
  -PI/2 < atan x - atan y < PI/2.

Lemma Machin_2_3 : PI/4 = atan(/2) + atan(/3).

Lemma Machin_4_5_239 : PI/4 = 4 * atan (/5) - atan(/239).

Lemma Machin_2_3_7 : PI/4 = 2 * atan(/3) + (atan (/7)).


Definition PI_2_3_7_tg n :=
  2 * Ratan_seq (/3) n + Ratan_seq (/7) n.

Lemma PI_2_3_7_ineq :
  forall N : nat,
    sum_f_R0 (tg_alt PI_2_3_7_tg) (S (2 * N)) <= PI / 4 <=
    sum_f_R0 (tg_alt PI_2_3_7_tg) (2 * N).