Library Stdlib.Reals.Machin

From Stdlib Require Import Lia.
From Stdlib Require Import Lra.
From Stdlib Require Import Rbase.
From Stdlib Require Import Rtrigo1.
From Stdlib Require Import Ranalysis_reg.
From Stdlib Require Import Rfunctions.
From Stdlib Require Import AltSeries.
From Stdlib Require Import Rseries.
From Stdlib Require Import SeqProp.
From Stdlib Require Import PartSum.
From Stdlib 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).