# Library Coq.Reals.Machin

Require Import Fourier.
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).