Machin.v

Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.
(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

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.
Require Import Omega.

Local Open Scope R_scope.

(* Proving a few formulas in the style of John Machin to compute Pi *)

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).forall u v : R,
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)
Proof.forall u v : R,
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)
intros u v pn0 uvint aint.u, v:R
pn0:1 + u * v <> 0
uvint:- PI / 2 < atan u - atan v < PI / 2
aint:- PI / 2 < atan (atan_sub u v) < PI / 2
atan u = atan v + atan (atan_sub u v)
assert (cos (atan u) <> 0).u, v:R
pn0:1 + u * v <> 0
uvint:- PI / 2 < atan u - atan v < PI / 2
aint:- PI / 2 < atan (atan_sub u v) < PI / 2
cos (atan u) <> 0
u, v:R
pn0:1 + u * v <> 0
uvint:- PI / 2 < atan u - atan v < PI / 2
aint:- PI / 2 < atan (atan_sub u v) < PI / 2
H:cos (atan u) <> 0
atan u = atan v + atan (atan_sub u v)
 destruct (atan_bound u); apply Rgt_not_eq, cos_gt_0; auto.u, v:R
pn0:1 + u * v <> 0
uvint:- PI / 2 < atan u - atan v < PI / 2
aint:- PI / 2 < atan (atan_sub u v) < PI / 2
H:- PI / 2 < atan u
H0:atan u < PI / 2
- (PI / 2) < atan u
u, v:R
pn0:1 + u * v <> 0
uvint:- PI / 2 < atan u - atan v < PI / 2
aint:- PI / 2 < atan (atan_sub u v) < PI / 2
H:cos (atan u) <> 0
atan u = atan v + atan (atan_sub u v)
 rewrite <- Ropp_div; assumption.u, v:R
pn0:1 + u * v <> 0
uvint:- PI / 2 < atan u - atan v < PI / 2
aint:- PI / 2 < atan (atan_sub u v) < PI / 2
H:cos (atan u) <> 0
atan u = atan v + atan (atan_sub u v)
assert (cos (atan v) <> 0).u, v:R
pn0:1 + u * v <> 0
uvint:- PI / 2 < atan u - atan v < PI / 2
aint:- PI / 2 < atan (atan_sub u v) < PI / 2
H:cos (atan u) <> 0
cos (atan v) <> 0
u, v:R
pn0:1 + u * v <> 0
uvint:- PI / 2 < atan u - atan v < PI / 2
aint:- PI / 2 < atan (atan_sub u v) < PI / 2
H:cos (atan u) <> 0
H0:cos (atan v) <> 0
atan u = atan v + atan (atan_sub u v)
 destruct (atan_bound v); apply Rgt_not_eq, cos_gt_0; auto.u, v:R
pn0:1 + u * v <> 0
uvint:- PI / 2 < atan u - atan v < PI / 2
aint:- PI / 2 < atan (atan_sub u v) < PI / 2
H:cos (atan u) <> 0
H0:- PI / 2 < atan v
H1:atan v < PI / 2
- (PI / 2) < atan v
u, v:R
pn0:1 + u * v <> 0
uvint:- PI / 2 < atan u - atan v < PI / 2
aint:- PI / 2 < atan (atan_sub u v) < PI / 2
H:cos (atan u) <> 0
H0:cos (atan v) <> 0
atan u = atan v + atan (atan_sub u v)
 rewrite <- Ropp_div; assumption.u, v:R
pn0:1 + u * v <> 0
uvint:- PI / 2 < atan u - atan v < PI / 2
aint:- PI / 2 < atan (atan_sub u v) < PI / 2
H:cos (atan u) <> 0
H0:cos (atan v) <> 0
atan u = atan v + atan (atan_sub u v)
assert (t : forall a b c, a - b = c -> a = b + c) by (intros; subst; field).u, v:R
pn0:1 + u * v <> 0
uvint:- PI / 2 < atan u - atan v < PI / 2
aint:- PI / 2 < atan (atan_sub u v) < PI / 2
H:cos (atan u) <> 0
H0:cos (atan v) <> 0
t:forall a b c : R, a - b = c -> a = b + c
atan u = atan v + atan (atan_sub u v)
apply t, tan_is_inj; clear t; try assumption.u, v:R
pn0:1 + u * v <> 0
uvint:- PI / 2 < atan u - atan v < PI / 2
aint:- PI / 2 < atan (atan_sub u v) < PI / 2
H:cos (atan u) <> 0
H0:cos (atan v) <> 0
tan (atan u - atan v) = tan (atan (atan_sub u v))
rewrite tan_minus; auto.u, v:R
pn0:1 + u * v <> 0
uvint:- PI / 2 < atan u - atan v < PI / 2
aint:- PI / 2 < atan (atan_sub u v) < PI / 2
H:cos (atan u) <> 0
H0:cos (atan v) <> 0
(tan (atan u) - tan (atan v)) /
(1 + tan (atan u) * tan (atan v)) =
tan (atan (atan_sub u v))
u, v:R
pn0:1 + u * v <> 0
uvint:- PI / 2 < atan u - atan v < PI / 2
aint:- PI / 2 < atan (atan_sub u v) < PI / 2
H:cos (atan u) <> 0
H0:cos (atan v) <> 0
cos (atan u - atan v) <> 0
u, v:R
pn0:1 + u * v <> 0
uvint:- PI / 2 < atan u - atan v < PI / 2
aint:- PI / 2 < atan (atan_sub u v) < PI / 2
H:cos (atan u) <> 0
H0:cos (atan v) <> 0
1 + tan (atan u) * tan (atan v) <> 0
  rewrite !atan_right_inv; reflexivity.u, v:R
pn0:1 + u * v <> 0
uvint:- PI / 2 < atan u - atan v < PI / 2
aint:- PI / 2 < atan (atan_sub u v) < PI / 2
H:cos (atan u) <> 0
H0:cos (atan v) <> 0
cos (atan u - atan v) <> 0
u, v:R
pn0:1 + u * v <> 0
uvint:- PI / 2 < atan u - atan v < PI / 2
aint:- PI / 2 < atan (atan_sub u v) < PI / 2
H:cos (atan u) <> 0
H0:cos (atan v) <> 0
1 + tan (atan u) * tan (atan v) <> 0
apply Rgt_not_eq, cos_gt_0; rewrite <- ?Ropp_div; tauto.u, v:R
pn0:1 + u * v <> 0
uvint:- PI / 2 < atan u - atan v < PI / 2
aint:- PI / 2 < atan (atan_sub u v) < PI / 2
H:cos (atan u) <> 0
H0:cos (atan v) <> 0
1 + tan (atan u) * tan (atan v) <> 0
rewrite !atan_right_inv; assumption.
Qed.

Lemma tech : forall x y , -1 <= x <= 1 -> -1 < y < 1 -> 
  -PI/2 < atan x - atan y < PI/2.forall x y : R,
-1 <= x <= 1 ->
-1 < y < 1 -> - PI / 2 < atan x - atan y < PI / 2
Proof.forall x y : R,
-1 <= x <= 1 ->
-1 < y < 1 -> - PI / 2 < atan x - atan y < PI / 2
assert (ut := PI_RGT_0).ut:PI > 0
forall x y : R,
-1 <= x <= 1 ->
-1 < y < 1 -> - PI / 2 < atan x - atan y < PI / 2
intros x y [xm1 x1] [ym1 y1].ut:PI > 0
x, y:R
xm1:-1 <= x
x1:x <= 1
ym1:-1 < y
y1:y < 1
- PI / 2 < atan x - atan y < PI / 2
assert (-(PI/4) <= atan x).ut:PI > 0
x, y:R
xm1:-1 <= x
x1:x <= 1
ym1:-1 < y
y1:y < 1
- (PI / 4) <= atan x
ut:PI > 0
x, y:R
xm1:-1 <= x
x1:x <= 1
ym1:-1 < y
y1:y < 1
H:- (PI / 4) <= atan x
- PI / 2 < atan x - atan y < PI / 2
 destruct xm1 as [xm1 | xm1].ut:PI > 0
x, y:R
xm1:-1 < x
x1:x <= 1
ym1:-1 < y
y1:y < 1
- (PI / 4) <= atan x
ut:PI > 0
x, y:R
xm1:-1 = x
x1:x <= 1
ym1:-1 < y
y1:y < 1
- (PI / 4) <= atan x
ut:PI > 0
x, y:R
xm1:-1 <= x
x1:x <= 1
ym1:-1 < y
y1:y < 1
H:- (PI / 4) <= atan x
- PI / 2 < atan x - atan y < PI / 2
  rewrite <- atan_1, <- atan_opp; apply Rlt_le, atan_increasing.ut:PI > 0
x, y:R
xm1:-1 < x
x1:x <= 1
ym1:-1 < y
y1:y < 1
- (1) < x
ut:PI > 0
x, y:R
xm1:-1 = x
x1:x <= 1
ym1:-1 < y
y1:y < 1
- (PI / 4) <= atan x
ut:PI > 0
x, y:R
xm1:-1 <= x
x1:x <= 1
ym1:-1 < y
y1:y < 1
H:- (PI / 4) <= atan x
- PI / 2 < atan x - atan y < PI / 2
  assumption.ut:PI > 0
x, y:R
xm1:-1 = x
x1:x <= 1
ym1:-1 < y
y1:y < 1
- (PI / 4) <= atan x
ut:PI > 0
x, y:R
xm1:-1 <= x
x1:x <= 1
ym1:-1 < y
y1:y < 1
H:- (PI / 4) <= atan x
- PI / 2 < atan x - atan y < PI / 2
 solve[rewrite <- xm1; change (-1) with (-(1)); rewrite atan_opp, atan_1; apply Rle_refl].ut:PI > 0
x, y:R
xm1:-1 <= x
x1:x <= 1
ym1:-1 < y
y1:y < 1
H:- (PI / 4) <= atan x
- PI / 2 < atan x - atan y < PI / 2
assert (-(PI/4) < atan y).ut:PI > 0
x, y:R
xm1:-1 <= x
x1:x <= 1
ym1:-1 < y
y1:y < 1
H:- (PI / 4) <= atan x
- (PI / 4) < atan y
ut:PI > 0
x, y:R
xm1:-1 <= x
x1:x <= 1
ym1:-1 < y
y1:y < 1
H:- (PI / 4) <= atan x
H0:- (PI / 4) < atan y
- PI / 2 < atan x - atan y < PI / 2
 rewrite <- atan_1, <- atan_opp; apply atan_increasing.ut:PI > 0
x, y:R
xm1:-1 <= x
x1:x <= 1
ym1:-1 < y
y1:y < 1
H:- (PI / 4) <= atan x
- (1) < y
ut:PI > 0
x, y:R
xm1:-1 <= x
x1:x <= 1
ym1:-1 < y
y1:y < 1
H:- (PI / 4) <= atan x
H0:- (PI / 4) < atan y
- PI / 2 < atan x - atan y < PI / 2
 assumption.ut:PI > 0
x, y:R
xm1:-1 <= x
x1:x <= 1
ym1:-1 < y
y1:y < 1
H:- (PI / 4) <= atan x
H0:- (PI / 4) < atan y
- PI / 2 < atan x - atan y < PI / 2
assert (atan x <= PI/4).ut:PI > 0
x, y:R
xm1:-1 <= x
x1:x <= 1
ym1:-1 < y
y1:y < 1
H:- (PI / 4) <= atan x
H0:- (PI / 4) < atan y
atan x <= PI / 4
ut:PI > 0
x, y:R
xm1:-1 <= x
x1:x <= 1
ym1:-1 < y
y1:y < 1
H:- (PI / 4) <= atan x
H0:- (PI / 4) < atan y
H1:atan x <= PI / 4
- PI / 2 < atan x - atan y < PI / 2
 destruct x1 as [x1 | x1].ut:PI > 0
x, y:R
xm1:-1 <= x
x1:x < 1
ym1:-1 < y
y1:y < 1
H:- (PI / 4) <= atan x
H0:- (PI / 4) < atan y
atan x <= PI / 4
ut:PI > 0
x, y:R
xm1:-1 <= x
x1:x = 1
ym1:-1 < y
y1:y < 1
H:- (PI / 4) <= atan x
H0:- (PI / 4) < atan y
atan x <= PI / 4
ut:PI > 0
x, y:R
xm1:-1 <= x
x1:x <= 1
ym1:-1 < y
y1:y < 1
H:- (PI / 4) <= atan x
H0:- (PI / 4) < atan y
H1:atan x <= PI / 4
- PI / 2 < atan x - atan y < PI / 2
  rewrite <- atan_1; apply Rlt_le, atan_increasing.ut:PI > 0
x, y:R
xm1:-1 <= x
x1:x < 1
ym1:-1 < y
y1:y < 1
H:- (PI / 4) <= atan x
H0:- (PI / 4) < atan y
x < 1
ut:PI > 0
x, y:R
xm1:-1 <= x
x1:x = 1
ym1:-1 < y
y1:y < 1
H:- (PI / 4) <= atan x
H0:- (PI / 4) < atan y
atan x <= PI / 4
ut:PI > 0
x, y:R
xm1:-1 <= x
x1:x <= 1
ym1:-1 < y
y1:y < 1
H:- (PI / 4) <= atan x
H0:- (PI / 4) < atan y
H1:atan x <= PI / 4
- PI / 2 < atan x - atan y < PI / 2
  assumption.ut:PI > 0
x, y:R
xm1:-1 <= x
x1:x = 1
ym1:-1 < y
y1:y < 1
H:- (PI / 4) <= atan x
H0:- (PI / 4) < atan y
atan x <= PI / 4
ut:PI > 0
x, y:R
xm1:-1 <= x
x1:x <= 1
ym1:-1 < y
y1:y < 1
H:- (PI / 4) <= atan x
H0:- (PI / 4) < atan y
H1:atan x <= PI / 4
- PI / 2 < atan x - atan y < PI / 2
 solve[rewrite x1, atan_1; apply Rle_refl].ut:PI > 0
x, y:R
xm1:-1 <= x
x1:x <= 1
ym1:-1 < y
y1:y < 1
H:- (PI / 4) <= atan x
H0:- (PI / 4) < atan y
H1:atan x <= PI / 4
- PI / 2 < atan x - atan y < PI / 2
assert (atan y < PI/4).ut:PI > 0
x, y:R
xm1:-1 <= x
x1:x <= 1
ym1:-1 < y
y1:y < 1
H:- (PI / 4) <= atan x
H0:- (PI / 4) < atan y
H1:atan x <= PI / 4
atan y < PI / 4
ut:PI > 0
x, y:R
xm1:-1 <= x
x1:x <= 1
ym1:-1 < y
y1:y < 1
H:- (PI / 4) <= atan x
H0:- (PI / 4) < atan y
H1:atan x <= PI / 4
H2:atan y < PI / 4
- PI / 2 < atan x - atan y < PI / 2
  rewrite <- atan_1; apply atan_increasing.ut:PI > 0
x, y:R
xm1:-1 <= x
x1:x <= 1
ym1:-1 < y
y1:y < 1
H:- (PI / 4) <= atan x
H0:- (PI / 4) < atan y
H1:atan x <= PI / 4
y < 1
ut:PI > 0
x, y:R
xm1:-1 <= x
x1:x <= 1
ym1:-1 < y
y1:y < 1
H:- (PI / 4) <= atan x
H0:- (PI / 4) < atan y
H1:atan x <= PI / 4
H2:atan y < PI / 4
- PI / 2 < atan x - atan y < PI / 2
  assumption.ut:PI > 0
x, y:R
xm1:-1 <= x
x1:x <= 1
ym1:-1 < y
y1:y < 1
H:- (PI / 4) <= atan x
H0:- (PI / 4) < atan y
H1:atan x <= PI / 4
H2:atan y < PI / 4
- PI / 2 < atan x - atan y < PI / 2
rewrite Ropp_div; split; lra.
Qed.

(* A simple formula, reasonably efficient. *)
Lemma Machin_2_3 : PI/4 = atan(/2) + atan(/3).PI / 4 = atan (/ 2) + atan (/ 3)
Proof.PI / 4 = atan (/ 2) + atan (/ 3)
assert (utility : 0 < PI/2) by (apply PI2_RGT_0).utility:0 < PI / 2
PI / 4 = atan (/ 2) + atan (/ 3)
rewrite <- atan_1.utility:0 < PI / 2
atan 1 = atan (/ 2) + atan (/ 3)
rewrite (atan_sub_correct 1 (/2)).utility:0 < PI / 2
atan (/ 2) + atan (atan_sub 1 (/ 2)) =
atan (/ 2) + atan (/ 3)
utility:0 < PI / 2
1 + 1 * / 2 <> 0
utility:0 < PI / 2
- PI / 2 < atan 1 - atan (/ 2) < PI / 2
utility:0 < PI / 2
- PI / 2 < atan (atan_sub 1 (/ 2)) < PI / 2
   apply f_equal, f_equal; unfold atan_sub; field.utility:0 < PI / 2
1 + 1 * / 2 <> 0
utility:0 < PI / 2
- PI / 2 < atan 1 - atan (/ 2) < PI / 2
utility:0 < PI / 2
- PI / 2 < atan (atan_sub 1 (/ 2)) < PI / 2
  apply Rgt_not_eq; lra.utility:0 < PI / 2
- PI / 2 < atan 1 - atan (/ 2) < PI / 2
utility:0 < PI / 2
- PI / 2 < atan (atan_sub 1 (/ 2)) < PI / 2
 apply tech; try split; try lra.utility:0 < PI / 2
- PI / 2 < atan (atan_sub 1 (/ 2)) < PI / 2
apply atan_bound.
Qed.

Lemma Machin_4_5_239 : PI/4 = 4 * atan (/5) - atan(/239).PI / 4 = 4 * atan (/ 5) - atan (/ 239)
Proof.PI / 4 = 4 * atan (/ 5) - atan (/ 239)
rewrite <- atan_1.atan 1 = 4 * atan (/ 5) - atan (/ 239)
rewrite (atan_sub_correct 1 (/5));
 [ | apply Rgt_not_eq; lra | apply tech; try split; lra |
     apply atan_bound ].atan (/ 5) + atan (atan_sub 1 (/ 5)) =
4 * atan (/ 5) - atan (/ 239)
replace (4 * atan (/5) - atan (/239)) with
  (atan (/5) + (atan (/5) + (atan (/5) + (atan (/5) + -
     atan (/239))))) by ring.atan (/ 5) + atan (atan_sub 1 (/ 5)) =
atan (/ 5) +
(atan (/ 5) +
 (atan (/ 5) + (atan (/ 5) + - atan (/ 239))))
apply f_equal.atan (atan_sub 1 (/ 5)) =
atan (/ 5) +
(atan (/ 5) + (atan (/ 5) + - atan (/ 239)))
replace (atan_sub 1 (/5)) with (2/3) by
  (unfold atan_sub; field).atan (2 / 3) =
atan (/ 5) +
(atan (/ 5) + (atan (/ 5) + - atan (/ 239)))
rewrite (atan_sub_correct (2/3) (/5));
 [apply f_equal | apply Rgt_not_eq; lra | apply tech; try split; lra |
     apply atan_bound ].atan (atan_sub (2 / 3) (/ 5)) =
atan (/ 5) + (atan (/ 5) + - atan (/ 239))
replace (atan_sub (2/3) (/5)) with (7/17)  by
  (unfold atan_sub; field).atan (7 / 17) =
atan (/ 5) + (atan (/ 5) + - atan (/ 239))
rewrite (atan_sub_correct (7/17) (/5));
 [apply f_equal | apply Rgt_not_eq; lra | apply tech; try split; lra |
     apply atan_bound ].atan (atan_sub (7 / 17) (/ 5)) =
atan (/ 5) + - atan (/ 239)
replace (atan_sub (7/17) (/5)) with (9/46) by
  (unfold atan_sub; field).atan (9 / 46) = atan (/ 5) + - atan (/ 239)
rewrite (atan_sub_correct (9/46) (/5));
 [apply f_equal | apply Rgt_not_eq; lra | apply tech; try split; lra |
     apply atan_bound ].atan (atan_sub (9 / 46) (/ 5)) = - atan (/ 239)
rewrite <- atan_opp; apply f_equal.atan_sub (9 / 46) (/ 5) = - / 239
unfold atan_sub; field.
Qed.

Lemma Machin_2_3_7 : PI/4 = 2 * atan(/3) + (atan (/7)).PI / 4 = 2 * atan (/ 3) + atan (/ 7)
Proof.PI / 4 = 2 * atan (/ 3) + atan (/ 7)
rewrite <- atan_1.atan 1 = 2 * atan (/ 3) + atan (/ 7)
rewrite (atan_sub_correct 1 (/3));
 [ | apply Rgt_not_eq; lra | apply tech; try split; lra |
     apply atan_bound ].atan (/ 3) + atan (atan_sub 1 (/ 3)) =
2 * atan (/ 3) + atan (/ 7)
replace (2 * atan (/3) + atan (/7)) with
  (atan (/3) + (atan (/3) + atan (/7))) by ring.atan (/ 3) + atan (atan_sub 1 (/ 3)) =
atan (/ 3) + (atan (/ 3) + atan (/ 7))
apply f_equal.atan (atan_sub 1 (/ 3)) = atan (/ 3) + atan (/ 7)
replace (atan_sub 1 (/3)) with (/2) by
  (unfold atan_sub; field).atan (/ 2) = atan (/ 3) + atan (/ 7)
rewrite (atan_sub_correct (/2) (/3));
 [apply f_equal | apply Rgt_not_eq; lra | apply tech; try split; lra |
     apply atan_bound ].atan (atan_sub (/ 2) (/ 3)) = atan (/ 7)
apply f_equal; unfold atan_sub; field.
Qed.

(* More efficient way to compute approximations of PI. *)

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).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)
Proof.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)
assert (dec3 : 0 <= /3 <= 1) by (split; lra).dec3:0 <= / 3 <= 1
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)
assert (dec7 : 0 <= /7 <= 1) by (split; lra).dec3:0 <= / 3 <= 1
dec7:0 <= / 7 <= 1
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)
assert (decr : Un_decreasing PI_2_3_7_tg).dec3:0 <= / 3 <= 1
dec7:0 <= / 7 <= 1
Un_decreasing PI_2_3_7_tg
dec3:0 <= / 3 <= 1
dec7:0 <= / 7 <= 1
decr:Un_decreasing PI_2_3_7_tg
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)
 apply Ratan_seq_decreasing in dec3.dec3:Un_decreasing (Ratan_seq (/ 3))
dec7:0 <= / 7 <= 1
Un_decreasing PI_2_3_7_tg
dec3:0 <= / 3 <= 1
dec7:0 <= / 7 <= 1
decr:Un_decreasing PI_2_3_7_tg
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)
 apply Ratan_seq_decreasing in dec7.dec3:Un_decreasing (Ratan_seq (/ 3))
dec7:Un_decreasing (Ratan_seq (/ 7))
Un_decreasing PI_2_3_7_tg
dec3:0 <= / 3 <= 1
dec7:0 <= / 7 <= 1
decr:Un_decreasing PI_2_3_7_tg
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)
 intros n; apply Rplus_le_compat.dec3:Un_decreasing (Ratan_seq (/ 3))
dec7:Un_decreasing (Ratan_seq (/ 7))
n:nat
2 * Ratan_seq (/ 3) (S n) <= 2 * Ratan_seq (/ 3) n
dec3:Un_decreasing (Ratan_seq (/ 3))
dec7:Un_decreasing (Ratan_seq (/ 7))
n:nat
Ratan_seq (/ 7) (S n) <= Ratan_seq (/ 7) n
dec3:0 <= / 3 <= 1
dec7:0 <= / 7 <= 1
decr:Un_decreasing PI_2_3_7_tg
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)
  apply Rmult_le_compat_l; [ lra | exact (dec3 n)].dec3:Un_decreasing (Ratan_seq (/ 3))
dec7:Un_decreasing (Ratan_seq (/ 7))
n:nat
Ratan_seq (/ 7) (S n) <= Ratan_seq (/ 7) n
dec3:0 <= / 3 <= 1
dec7:0 <= / 7 <= 1
decr:Un_decreasing PI_2_3_7_tg
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)
 exact (dec7 n).dec3:0 <= / 3 <= 1
dec7:0 <= / 7 <= 1
decr:Un_decreasing PI_2_3_7_tg
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)
assert (cv : Un_cv PI_2_3_7_tg 0).dec3:0 <= / 3 <= 1
dec7:0 <= / 7 <= 1
decr:Un_decreasing PI_2_3_7_tg
Un_cv PI_2_3_7_tg 0
dec3:0 <= / 3 <= 1
dec7:0 <= / 7 <= 1
decr:Un_decreasing PI_2_3_7_tg
cv:Un_cv PI_2_3_7_tg 0
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)
 apply Ratan_seq_converging in dec3.dec3:Un_cv (Ratan_seq (/ 3)) 0
dec7:0 <= / 7 <= 1
decr:Un_decreasing PI_2_3_7_tg
Un_cv PI_2_3_7_tg 0
dec3:0 <= / 3 <= 1
dec7:0 <= / 7 <= 1
decr:Un_decreasing PI_2_3_7_tg
cv:Un_cv PI_2_3_7_tg 0
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)
 apply Ratan_seq_converging in dec7.dec3:Un_cv (Ratan_seq (/ 3)) 0
dec7:Un_cv (Ratan_seq (/ 7)) 0
decr:Un_decreasing PI_2_3_7_tg
Un_cv PI_2_3_7_tg 0
dec3:0 <= / 3 <= 1
dec7:0 <= / 7 <= 1
decr:Un_decreasing PI_2_3_7_tg
cv:Un_cv PI_2_3_7_tg 0
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)
 intros eps ep.dec3:Un_cv (Ratan_seq (/ 3)) 0
dec7:Un_cv (Ratan_seq (/ 7)) 0
decr:Un_decreasing PI_2_3_7_tg
eps:R
ep:eps > 0
exists N : nat,
  forall n : nat,
  (n >= N)%nat -> R_dist (PI_2_3_7_tg n) 0 < eps
dec3:0 <= / 3 <= 1
dec7:0 <= / 7 <= 1
decr:Un_decreasing PI_2_3_7_tg
cv:Un_cv PI_2_3_7_tg 0
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)
 assert (ep' : 0 < eps /3) by lra.dec3:Un_cv (Ratan_seq (/ 3)) 0
dec7:Un_cv (Ratan_seq (/ 7)) 0
decr:Un_decreasing PI_2_3_7_tg
eps:R
ep:eps > 0
ep':0 < eps / 3
exists N : nat,
  forall n : nat,
  (n >= N)%nat -> R_dist (PI_2_3_7_tg n) 0 < eps
dec3:0 <= / 3 <= 1
dec7:0 <= / 7 <= 1
decr:Un_decreasing PI_2_3_7_tg
cv:Un_cv PI_2_3_7_tg 0
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)
 destruct (dec3 _ ep') as [N1 Pn1]; destruct (dec7 _ ep') as [N2 Pn2].dec3:Un_cv (Ratan_seq (/ 3)) 0
dec7:Un_cv (Ratan_seq (/ 7)) 0
decr:Un_decreasing PI_2_3_7_tg
eps:R
ep:eps > 0
ep':0 < eps / 3
N1:nat
Pn1:forall n : nat,
(n >= N1)%nat ->
R_dist (Ratan_seq (/ 3) n) 0 < eps / 3
N2:nat
Pn2:forall n : nat,
(n >= N2)%nat ->
R_dist (Ratan_seq (/ 7) n) 0 < eps / 3
exists N : nat,
  forall n : nat,
  (n >= N)%nat -> R_dist (PI_2_3_7_tg n) 0 < eps
dec3:0 <= / 3 <= 1
dec7:0 <= / 7 <= 1
decr:Un_decreasing PI_2_3_7_tg
cv:Un_cv PI_2_3_7_tg 0
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)
 exists (N1 + N2)%nat; intros n Nn.dec3:Un_cv (Ratan_seq (/ 3)) 0
dec7:Un_cv (Ratan_seq (/ 7)) 0
decr:Un_decreasing PI_2_3_7_tg
eps:R
ep:eps > 0
ep':0 < eps / 3
N1:nat
Pn1:forall n0 : nat,
(n0 >= N1)%nat ->
R_dist (Ratan_seq (/ 3) n0) 0 < eps / 3
N2:nat
Pn2:forall n0 : nat,
(n0 >= N2)%nat ->
R_dist (Ratan_seq (/ 7) n0) 0 < eps / 3
n:nat
Nn:(n >= N1 + N2)%nat
R_dist (PI_2_3_7_tg n) 0 < eps
dec3:0 <= / 3 <= 1
dec7:0 <= / 7 <= 1
decr:Un_decreasing PI_2_3_7_tg
cv:Un_cv PI_2_3_7_tg 0
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)
 unfold PI_2_3_7_tg.dec3:Un_cv (Ratan_seq (/ 3)) 0
dec7:Un_cv (Ratan_seq (/ 7)) 0
decr:Un_decreasing PI_2_3_7_tg
eps:R
ep:eps > 0
ep':0 < eps / 3
N1:nat
Pn1:forall n0 : nat,
(n0 >= N1)%nat ->
R_dist (Ratan_seq (/ 3) n0) 0 < eps / 3
N2:nat
Pn2:forall n0 : nat,
(n0 >= N2)%nat ->
R_dist (Ratan_seq (/ 7) n0) 0 < eps / 3
n:nat
Nn:(n >= N1 + N2)%nat
R_dist (2 * Ratan_seq (/ 3) n + Ratan_seq (/ 7) n) 0 <
eps
dec3:0 <= / 3 <= 1
dec7:0 <= / 7 <= 1
decr:Un_decreasing PI_2_3_7_tg
cv:Un_cv PI_2_3_7_tg 0
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)
 rewrite <- (Rplus_0_l 0).dec3:Un_cv (Ratan_seq (/ 3)) 0
dec7:Un_cv (Ratan_seq (/ 7)) 0
decr:Un_decreasing PI_2_3_7_tg
eps:R
ep:eps > 0
ep':0 < eps / 3
N1:nat
Pn1:forall n0 : nat,
(n0 >= N1)%nat ->
R_dist (Ratan_seq (/ 3) n0) 0 < eps / 3
N2:nat
Pn2:forall n0 : nat,
(n0 >= N2)%nat ->
R_dist (Ratan_seq (/ 7) n0) 0 < eps / 3
n:nat
Nn:(n >= N1 + N2)%nat
R_dist (2 * Ratan_seq (/ 3) n + Ratan_seq (/ 7) n)
  (0 + 0) < eps
dec3:0 <= / 3 <= 1
dec7:0 <= / 7 <= 1
decr:Un_decreasing PI_2_3_7_tg
cv:Un_cv PI_2_3_7_tg 0
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)
 apply Rle_lt_trans with
    (1 := R_dist_plus (2 * Ratan_seq (/3) n) 0 (Ratan_seq (/7) n) 0).dec3:Un_cv (Ratan_seq (/ 3)) 0
dec7:Un_cv (Ratan_seq (/ 7)) 0
decr:Un_decreasing PI_2_3_7_tg
eps:R
ep:eps > 0
ep':0 < eps / 3
N1:nat
Pn1:forall n0 : nat,
(n0 >= N1)%nat ->
R_dist (Ratan_seq (/ 3) n0) 0 < eps / 3
N2:nat
Pn2:forall n0 : nat,
(n0 >= N2)%nat ->
R_dist (Ratan_seq (/ 7) n0) 0 < eps / 3
n:nat
Nn:(n >= N1 + N2)%nat
R_dist (2 * Ratan_seq (/ 3) n) 0 +
R_dist (Ratan_seq (/ 7) n) 0 < eps
dec3:0 <= / 3 <= 1
dec7:0 <= / 7 <= 1
decr:Un_decreasing PI_2_3_7_tg
cv:Un_cv PI_2_3_7_tg 0
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)
 replace eps with (2 * eps/3 + eps/3) by field.dec3:Un_cv (Ratan_seq (/ 3)) 0
dec7:Un_cv (Ratan_seq (/ 7)) 0
decr:Un_decreasing PI_2_3_7_tg
eps:R
ep:eps > 0
ep':0 < eps / 3
N1:nat
Pn1:forall n0 : nat,
(n0 >= N1)%nat ->
R_dist (Ratan_seq (/ 3) n0) 0 < eps / 3
N2:nat
Pn2:forall n0 : nat,
(n0 >= N2)%nat ->
R_dist (Ratan_seq (/ 7) n0) 0 < eps / 3
n:nat
Nn:(n >= N1 + N2)%nat
R_dist (2 * Ratan_seq (/ 3) n) 0 +
R_dist (Ratan_seq (/ 7) n) 0 < 
2 * eps / 3 + eps / 3
dec3:0 <= / 3 <= 1
dec7:0 <= / 7 <= 1
decr:Un_decreasing PI_2_3_7_tg
cv:Un_cv PI_2_3_7_tg 0
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)
 apply Rplus_lt_compat.dec3:Un_cv (Ratan_seq (/ 3)) 0
dec7:Un_cv (Ratan_seq (/ 7)) 0
decr:Un_decreasing PI_2_3_7_tg
eps:R
ep:eps > 0
ep':0 < eps / 3
N1:nat
Pn1:forall n0 : nat,
(n0 >= N1)%nat ->
R_dist (Ratan_seq (/ 3) n0) 0 < eps / 3
N2:nat
Pn2:forall n0 : nat,
(n0 >= N2)%nat ->
R_dist (Ratan_seq (/ 7) n0) 0 < eps / 3
n:nat
Nn:(n >= N1 + N2)%nat
R_dist (2 * Ratan_seq (/ 3) n) 0 < 2 * eps / 3
dec3:Un_cv (Ratan_seq (/ 3)) 0
dec7:Un_cv (Ratan_seq (/ 7)) 0
decr:Un_decreasing PI_2_3_7_tg
eps:R
ep:eps > 0
ep':0 < eps / 3
N1:nat
Pn1:forall n0 : nat,
(n0 >= N1)%nat ->
R_dist (Ratan_seq (/ 3) n0) 0 < eps / 3
N2:nat
Pn2:forall n0 : nat,
(n0 >= N2)%nat ->
R_dist (Ratan_seq (/ 7) n0) 0 < eps / 3
n:nat
Nn:(n >= N1 + N2)%nat
R_dist (Ratan_seq (/ 7) n) 0 < eps / 3
dec3:0 <= / 3 <= 1
dec7:0 <= / 7 <= 1
decr:Un_decreasing PI_2_3_7_tg
cv:Un_cv PI_2_3_7_tg 0
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)
  unfold R_dist, Rminus, Rdiv.dec3:Un_cv (Ratan_seq (/ 3)) 0
dec7:Un_cv (Ratan_seq (/ 7)) 0
decr:Un_decreasing PI_2_3_7_tg
eps:R
ep:eps > 0
ep':0 < eps / 3
N1:nat
Pn1:forall n0 : nat,
(n0 >= N1)%nat ->
R_dist (Ratan_seq (/ 3) n0) 0 < eps / 3
N2:nat
Pn2:forall n0 : nat,
(n0 >= N2)%nat ->
R_dist (Ratan_seq (/ 7) n0) 0 < eps / 3
n:nat
Nn:(n >= N1 + N2)%nat
Rabs (2 * Ratan_seq (/ 3) n + - 0) < 2 * eps * / 3
dec3:Un_cv (Ratan_seq (/ 3)) 0
dec7:Un_cv (Ratan_seq (/ 7)) 0
decr:Un_decreasing PI_2_3_7_tg
eps:R
ep:eps > 0
ep':0 < eps / 3
N1:nat
Pn1:forall n0 : nat,
(n0 >= N1)%nat ->
R_dist (Ratan_seq (/ 3) n0) 0 < eps / 3
N2:nat
Pn2:forall n0 : nat,
(n0 >= N2)%nat ->
R_dist (Ratan_seq (/ 7) n0) 0 < eps / 3
n:nat
Nn:(n >= N1 + N2)%nat
R_dist (Ratan_seq (/ 7) n) 0 < eps / 3
dec3:0 <= / 3 <= 1
dec7:0 <= / 7 <= 1
decr:Un_decreasing PI_2_3_7_tg
cv:Un_cv PI_2_3_7_tg 0
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)
  rewrite <- (Rmult_0_r 2), <- Ropp_mult_distr_r_reverse.dec3:Un_cv (Ratan_seq (/ 3)) 0
dec7:Un_cv (Ratan_seq (/ 7)) 0
decr:Un_decreasing PI_2_3_7_tg
eps:R
ep:eps > 0
ep':0 < eps / 3
N1:nat
Pn1:forall n0 : nat,
(n0 >= N1)%nat ->
R_dist (Ratan_seq (/ 3) n0) 0 < eps / 3
N2:nat
Pn2:forall n0 : nat,
(n0 >= N2)%nat ->
R_dist (Ratan_seq (/ 7) n0) 0 < eps / 3
n:nat
Nn:(n >= N1 + N2)%nat
Rabs (2 * Ratan_seq (/ 3) n + 2 * - 0) < 2 * eps * / 3
dec3:Un_cv (Ratan_seq (/ 3)) 0
dec7:Un_cv (Ratan_seq (/ 7)) 0
decr:Un_decreasing PI_2_3_7_tg
eps:R
ep:eps > 0
ep':0 < eps / 3
N1:nat
Pn1:forall n0 : nat,
(n0 >= N1)%nat ->
R_dist (Ratan_seq (/ 3) n0) 0 < eps / 3
N2:nat
Pn2:forall n0 : nat,
(n0 >= N2)%nat ->
R_dist (Ratan_seq (/ 7) n0) 0 < eps / 3
n:nat
Nn:(n >= N1 + N2)%nat
R_dist (Ratan_seq (/ 7) n) 0 < eps / 3
dec3:0 <= / 3 <= 1
dec7:0 <= / 7 <= 1
decr:Un_decreasing PI_2_3_7_tg
cv:Un_cv PI_2_3_7_tg 0
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)
  rewrite <- Rmult_plus_distr_l, Rabs_mult, (Rabs_pos_eq 2);[|lra].dec3:Un_cv (Ratan_seq (/ 3)) 0
dec7:Un_cv (Ratan_seq (/ 7)) 0
decr:Un_decreasing PI_2_3_7_tg
eps:R
ep:eps > 0
ep':0 < eps / 3
N1:nat
Pn1:forall n0 : nat,
(n0 >= N1)%nat ->
R_dist (Ratan_seq (/ 3) n0) 0 < eps / 3
N2:nat
Pn2:forall n0 : nat,
(n0 >= N2)%nat ->
R_dist (Ratan_seq (/ 7) n0) 0 < eps / 3
n:nat
Nn:(n >= N1 + N2)%nat
2 * Rabs (Ratan_seq (/ 3) n + - 0) < 2 * eps * / 3
dec3:Un_cv (Ratan_seq (/ 3)) 0
dec7:Un_cv (Ratan_seq (/ 7)) 0
decr:Un_decreasing PI_2_3_7_tg
eps:R
ep:eps > 0
ep':0 < eps / 3
N1:nat
Pn1:forall n0 : nat,
(n0 >= N1)%nat ->
R_dist (Ratan_seq (/ 3) n0) 0 < eps / 3
N2:nat
Pn2:forall n0 : nat,
(n0 >= N2)%nat ->
R_dist (Ratan_seq (/ 7) n0) 0 < eps / 3
n:nat
Nn:(n >= N1 + N2)%nat
R_dist (Ratan_seq (/ 7) n) 0 < eps / 3
dec3:0 <= / 3 <= 1
dec7:0 <= / 7 <= 1
decr:Un_decreasing PI_2_3_7_tg
cv:Un_cv PI_2_3_7_tg 0
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)
  rewrite Rmult_assoc; apply Rmult_lt_compat_l;[lra | ].dec3:Un_cv (Ratan_seq (/ 3)) 0
dec7:Un_cv (Ratan_seq (/ 7)) 0
decr:Un_decreasing PI_2_3_7_tg
eps:R
ep:eps > 0
ep':0 < eps / 3
N1:nat
Pn1:forall n0 : nat,
(n0 >= N1)%nat ->
R_dist (Ratan_seq (/ 3) n0) 0 < eps / 3
N2:nat
Pn2:forall n0 : nat,
(n0 >= N2)%nat ->
R_dist (Ratan_seq (/ 7) n0) 0 < eps / 3
n:nat
Nn:(n >= N1 + N2)%nat
Rabs (Ratan_seq (/ 3) n + - 0) < eps * / 3
dec3:Un_cv (Ratan_seq (/ 3)) 0
dec7:Un_cv (Ratan_seq (/ 7)) 0
decr:Un_decreasing PI_2_3_7_tg
eps:R
ep:eps > 0
ep':0 < eps / 3
N1:nat
Pn1:forall n0 : nat,
(n0 >= N1)%nat ->
R_dist (Ratan_seq (/ 3) n0) 0 < eps / 3
N2:nat
Pn2:forall n0 : nat,
(n0 >= N2)%nat ->
R_dist (Ratan_seq (/ 7) n0) 0 < eps / 3
n:nat
Nn:(n >= N1 + N2)%nat
R_dist (Ratan_seq (/ 7) n) 0 < eps / 3
dec3:0 <= / 3 <= 1
dec7:0 <= / 7 <= 1
decr:Un_decreasing PI_2_3_7_tg
cv:Un_cv PI_2_3_7_tg 0
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)
   apply (Pn1 n); omega.dec3:Un_cv (Ratan_seq (/ 3)) 0
dec7:Un_cv (Ratan_seq (/ 7)) 0
decr:Un_decreasing PI_2_3_7_tg
eps:R
ep:eps > 0
ep':0 < eps / 3
N1:nat
Pn1:forall n0 : nat,
(n0 >= N1)%nat ->
R_dist (Ratan_seq (/ 3) n0) 0 < eps / 3
N2:nat
Pn2:forall n0 : nat,
(n0 >= N2)%nat ->
R_dist (Ratan_seq (/ 7) n0) 0 < eps / 3
n:nat
Nn:(n >= N1 + N2)%nat
R_dist (Ratan_seq (/ 7) n) 0 < eps / 3
dec3:0 <= / 3 <= 1
dec7:0 <= / 7 <= 1
decr:Un_decreasing PI_2_3_7_tg
cv:Un_cv PI_2_3_7_tg 0
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)
  apply (Pn2 n); omega.dec3:0 <= / 3 <= 1
dec7:0 <= / 7 <= 1
decr:Un_decreasing PI_2_3_7_tg
cv:Un_cv PI_2_3_7_tg 0
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)
rewrite Machin_2_3_7.dec3:0 <= / 3 <= 1
dec7:0 <= / 7 <= 1
decr:Un_decreasing PI_2_3_7_tg
cv:Un_cv PI_2_3_7_tg 0
forall N : nat,
sum_f_R0 (tg_alt PI_2_3_7_tg) (S (2 * N)) <=
2 * atan (/ 3) + atan (/ 7) <=
sum_f_R0 (tg_alt PI_2_3_7_tg) (2 * N)
rewrite !atan_eq_ps_atan; try (split; lra).dec3:0 <= / 3 <= 1
dec7:0 <= / 7 <= 1
decr:Un_decreasing PI_2_3_7_tg
cv:Un_cv PI_2_3_7_tg 0
forall N : nat,
sum_f_R0 (tg_alt PI_2_3_7_tg) (S (2 * N)) <=
2 * ps_atan (/ 3) + ps_atan (/ 7) <=
sum_f_R0 (tg_alt PI_2_3_7_tg) (2 * N)
unfold ps_atan; destruct (in_int (/3)); destruct (in_int (/7));
  try match goal with id : ~ _ |- _ => case id; split; lra end.dec3:0 <= / 3 <= 1
dec7:0 <= / 7 <= 1
decr:Un_decreasing PI_2_3_7_tg
cv:Un_cv PI_2_3_7_tg 0
a:-1 <= / 3 <= 1
a0:-1 <= / 7 <= 1
forall N : nat,
sum_f_R0 (tg_alt PI_2_3_7_tg) (S (2 * N)) <=
2 * (let (v, _) := ps_atan_exists_1 (/ 3) a in v) +
(let (v, _) := ps_atan_exists_1 (/ 7) a0 in v) <=
sum_f_R0 (tg_alt PI_2_3_7_tg) (2 * N)
destruct (ps_atan_exists_1 (/3)) as [v3 Pv3].dec3:0 <= / 3 <= 1
dec7:0 <= / 7 <= 1
decr:Un_decreasing PI_2_3_7_tg
cv:Un_cv PI_2_3_7_tg 0
a:-1 <= / 3 <= 1
a0:-1 <= / 7 <= 1
v3:R
Pv3:Un_cv
  (fun N : nat =>
   sum_f_R0 (tg_alt (Ratan_seq (/ 3))) N) v3
forall N : nat,
sum_f_R0 (tg_alt PI_2_3_7_tg) (S (2 * N)) <=
2 * v3 +
(let (v, _) := ps_atan_exists_1 (/ 7) a0 in v) <=
sum_f_R0 (tg_alt PI_2_3_7_tg) (2 * N)
destruct (ps_atan_exists_1 (/7)) as [v7 Pv7].dec3:0 <= / 3 <= 1
dec7:0 <= / 7 <= 1
decr:Un_decreasing PI_2_3_7_tg
cv:Un_cv PI_2_3_7_tg 0
a:-1 <= / 3 <= 1
a0:-1 <= / 7 <= 1
v3:R
Pv3:Un_cv
  (fun N : nat =>
   sum_f_R0 (tg_alt (Ratan_seq (/ 3))) N) v3
v7:R
Pv7:Un_cv
  (fun N : nat =>
   sum_f_R0 (tg_alt (Ratan_seq (/ 7))) N) v7
forall N : nat,
sum_f_R0 (tg_alt PI_2_3_7_tg) (S (2 * N)) <=
2 * v3 + v7 <= sum_f_R0 (tg_alt PI_2_3_7_tg) (2 * N)
assert (main : Un_cv (sum_f_R0 (tg_alt PI_2_3_7_tg)) (2 * v3 + v7)).dec3:0 <= / 3 <= 1
dec7:0 <= / 7 <= 1
decr:Un_decreasing PI_2_3_7_tg
cv:Un_cv PI_2_3_7_tg 0
a:-1 <= / 3 <= 1
a0:-1 <= / 7 <= 1
v3:R
Pv3:Un_cv
  (fun N : nat =>
   sum_f_R0 (tg_alt (Ratan_seq (/ 3))) N) v3
v7:R
Pv7:Un_cv
  (fun N : nat =>
   sum_f_R0 (tg_alt (Ratan_seq (/ 7))) N) v7
Un_cv (sum_f_R0 (tg_alt PI_2_3_7_tg)) (2 * v3 + v7)
dec3:0 <= / 3 <= 1
dec7:0 <= / 7 <= 1
decr:Un_decreasing PI_2_3_7_tg
cv:Un_cv PI_2_3_7_tg 0
a:-1 <= / 3 <= 1
a0:-1 <= / 7 <= 1
v3:R
Pv3:Un_cv
  (fun N : nat =>
   sum_f_R0 (tg_alt (Ratan_seq (/ 3))) N) v3
v7:R
Pv7:Un_cv
  (fun N : nat =>
   sum_f_R0 (tg_alt (Ratan_seq (/ 7))) N) v7
main:Un_cv (sum_f_R0 (tg_alt PI_2_3_7_tg))
  (2 * v3 + v7)
forall N : nat,
sum_f_R0 (tg_alt PI_2_3_7_tg) (S (2 * N)) <=
2 * v3 + v7 <= sum_f_R0 (tg_alt PI_2_3_7_tg) (2 * N)
 assert (main :Un_cv (fun n => 2 * sum_f_R0 (tg_alt (Ratan_seq (/3))) n +
                        sum_f_R0 (tg_alt (Ratan_seq (/7))) n) (2 * v3 + v7)).dec3:0 <= / 3 <= 1
dec7:0 <= / 7 <= 1
decr:Un_decreasing PI_2_3_7_tg
cv:Un_cv PI_2_3_7_tg 0
a:-1 <= / 3 <= 1
a0:-1 <= / 7 <= 1
v3:R
Pv3:Un_cv
  (fun N : nat =>
   sum_f_R0 (tg_alt (Ratan_seq (/ 3))) N) v3
v7:R
Pv7:Un_cv
  (fun N : nat =>
   sum_f_R0 (tg_alt (Ratan_seq (/ 7))) N) v7
Un_cv
  (fun n : nat =>
   2 * sum_f_R0 (tg_alt (Ratan_seq (/ 3))) n +
   sum_f_R0 (tg_alt (Ratan_seq (/ 7))) n)
  (2 * v3 + v7)
dec3:0 <= / 3 <= 1
dec7:0 <= / 7 <= 1
decr:Un_decreasing PI_2_3_7_tg
cv:Un_cv PI_2_3_7_tg 0
a:-1 <= / 3 <= 1
a0:-1 <= / 7 <= 1
v3:R
Pv3:Un_cv
  (fun N : nat =>
   sum_f_R0 (tg_alt (Ratan_seq (/ 3))) N) v3
v7:R
Pv7:Un_cv
  (fun N : nat =>
   sum_f_R0 (tg_alt (Ratan_seq (/ 7))) N) v7
main:Un_cv
  (fun n : nat =>
   2 * sum_f_R0 (tg_alt (Ratan_seq (/ 3))) n +
   sum_f_R0 (tg_alt (Ratan_seq (/ 7))) n)
  (2 * v3 + v7)
Un_cv (sum_f_R0 (tg_alt PI_2_3_7_tg)) (2 * v3 + v7)
dec3:0 <= / 3 <= 1
dec7:0 <= / 7 <= 1
decr:Un_decreasing PI_2_3_7_tg
cv:Un_cv PI_2_3_7_tg 0
a:-1 <= / 3 <= 1
a0:-1 <= / 7 <= 1
v3:R
Pv3:Un_cv
  (fun N : nat =>
   sum_f_R0 (tg_alt (Ratan_seq (/ 3))) N) v3
v7:R
Pv7:Un_cv
  (fun N : nat =>
   sum_f_R0 (tg_alt (Ratan_seq (/ 7))) N) v7
main:Un_cv (sum_f_R0 (tg_alt PI_2_3_7_tg))
  (2 * v3 + v7)
forall N : nat,
sum_f_R0 (tg_alt PI_2_3_7_tg) (S (2 * N)) <=
2 * v3 + v7 <= sum_f_R0 (tg_alt PI_2_3_7_tg) (2 * N)
  apply CV_plus;[ | assumption].dec3:0 <= / 3 <= 1
dec7:0 <= / 7 <= 1
decr:Un_decreasing PI_2_3_7_tg
cv:Un_cv PI_2_3_7_tg 0
a:-1 <= / 3 <= 1
a0:-1 <= / 7 <= 1
v3:R
Pv3:Un_cv
  (fun N : nat =>
   sum_f_R0 (tg_alt (Ratan_seq (/ 3))) N) v3
v7:R
Pv7:Un_cv
  (fun N : nat =>
   sum_f_R0 (tg_alt (Ratan_seq (/ 7))) N) v7
Un_cv
  (fun i : nat =>
   2 * sum_f_R0 (tg_alt (Ratan_seq (/ 3))) i) 
  (2 * v3)
dec3:0 <= / 3 <= 1
dec7:0 <= / 7 <= 1
decr:Un_decreasing PI_2_3_7_tg
cv:Un_cv PI_2_3_7_tg 0
a:-1 <= / 3 <= 1
a0:-1 <= / 7 <= 1
v3:R
Pv3:Un_cv
  (fun N : nat =>
   sum_f_R0 (tg_alt (Ratan_seq (/ 3))) N) v3
v7:R
Pv7:Un_cv
  (fun N : nat =>
   sum_f_R0 (tg_alt (Ratan_seq (/ 7))) N) v7
main:Un_cv
  (fun n : nat =>
   2 * sum_f_R0 (tg_alt (Ratan_seq (/ 3))) n +
   sum_f_R0 (tg_alt (Ratan_seq (/ 7))) n)
  (2 * v3 + v7)
Un_cv (sum_f_R0 (tg_alt PI_2_3_7_tg)) (2 * v3 + v7)
dec3:0 <= / 3 <= 1
dec7:0 <= / 7 <= 1
decr:Un_decreasing PI_2_3_7_tg
cv:Un_cv PI_2_3_7_tg 0
a:-1 <= / 3 <= 1
a0:-1 <= / 7 <= 1
v3:R
Pv3:Un_cv
  (fun N : nat =>
   sum_f_R0 (tg_alt (Ratan_seq (/ 3))) N) v3
v7:R
Pv7:Un_cv
  (fun N : nat =>
   sum_f_R0 (tg_alt (Ratan_seq (/ 7))) N) v7
main:Un_cv (sum_f_R0 (tg_alt PI_2_3_7_tg))
  (2 * v3 + v7)
forall N : nat,
sum_f_R0 (tg_alt PI_2_3_7_tg) (S (2 * N)) <=
2 * v3 + v7 <= sum_f_R0 (tg_alt PI_2_3_7_tg) (2 * N)
  apply CV_mult;[ | assumption].dec3:0 <= / 3 <= 1
dec7:0 <= / 7 <= 1
decr:Un_decreasing PI_2_3_7_tg
cv:Un_cv PI_2_3_7_tg 0
a:-1 <= / 3 <= 1
a0:-1 <= / 7 <= 1
v3:R
Pv3:Un_cv
  (fun N : nat =>
   sum_f_R0 (tg_alt (Ratan_seq (/ 3))) N) v3
v7:R
Pv7:Un_cv
  (fun N : nat =>
   sum_f_R0 (tg_alt (Ratan_seq (/ 7))) N) v7
Un_cv (fun _ : nat => 2) 2
dec3:0 <= / 3 <= 1
dec7:0 <= / 7 <= 1
decr:Un_decreasing PI_2_3_7_tg
cv:Un_cv PI_2_3_7_tg 0
a:-1 <= / 3 <= 1
a0:-1 <= / 7 <= 1
v3:R
Pv3:Un_cv
  (fun N : nat =>
   sum_f_R0 (tg_alt (Ratan_seq (/ 3))) N) v3
v7:R
Pv7:Un_cv
  (fun N : nat =>
   sum_f_R0 (tg_alt (Ratan_seq (/ 7))) N) v7
main:Un_cv
  (fun n : nat =>
   2 * sum_f_R0 (tg_alt (Ratan_seq (/ 3))) n +
   sum_f_R0 (tg_alt (Ratan_seq (/ 7))) n)
  (2 * v3 + v7)
Un_cv (sum_f_R0 (tg_alt PI_2_3_7_tg)) (2 * v3 + v7)
dec3:0 <= / 3 <= 1
dec7:0 <= / 7 <= 1
decr:Un_decreasing PI_2_3_7_tg
cv:Un_cv PI_2_3_7_tg 0
a:-1 <= / 3 <= 1
a0:-1 <= / 7 <= 1
v3:R
Pv3:Un_cv
  (fun N : nat =>
   sum_f_R0 (tg_alt (Ratan_seq (/ 3))) N) v3
v7:R
Pv7:Un_cv
  (fun N : nat =>
   sum_f_R0 (tg_alt (Ratan_seq (/ 7))) N) v7
main:Un_cv (sum_f_R0 (tg_alt PI_2_3_7_tg))
  (2 * v3 + v7)
forall N : nat,
sum_f_R0 (tg_alt PI_2_3_7_tg) (S (2 * N)) <=
2 * v3 + v7 <= sum_f_R0 (tg_alt PI_2_3_7_tg) (2 * N)
  exists 0%nat; intros; rewrite R_dist_eq; assumption.dec3:0 <= / 3 <= 1
dec7:0 <= / 7 <= 1
decr:Un_decreasing PI_2_3_7_tg
cv:Un_cv PI_2_3_7_tg 0
a:-1 <= / 3 <= 1
a0:-1 <= / 7 <= 1
v3:R
Pv3:Un_cv
  (fun N : nat =>
   sum_f_R0 (tg_alt (Ratan_seq (/ 3))) N) v3
v7:R
Pv7:Un_cv
  (fun N : nat =>
   sum_f_R0 (tg_alt (Ratan_seq (/ 7))) N) v7
main:Un_cv
  (fun n : nat =>
   2 * sum_f_R0 (tg_alt (Ratan_seq (/ 3))) n +
   sum_f_R0 (tg_alt (Ratan_seq (/ 7))) n)
  (2 * v3 + v7)
Un_cv (sum_f_R0 (tg_alt PI_2_3_7_tg)) (2 * v3 + v7)
dec3:0 <= / 3 <= 1
dec7:0 <= / 7 <= 1
decr:Un_decreasing PI_2_3_7_tg
cv:Un_cv PI_2_3_7_tg 0
a:-1 <= / 3 <= 1
a0:-1 <= / 7 <= 1
v3:R
Pv3:Un_cv
  (fun N : nat =>
   sum_f_R0 (tg_alt (Ratan_seq (/ 3))) N) v3
v7:R
Pv7:Un_cv
  (fun N : nat =>
   sum_f_R0 (tg_alt (Ratan_seq (/ 7))) N) v7
main:Un_cv (sum_f_R0 (tg_alt PI_2_3_7_tg))
  (2 * v3 + v7)
forall N : nat,
sum_f_R0 (tg_alt PI_2_3_7_tg) (S (2 * N)) <=
2 * v3 + v7 <= sum_f_R0 (tg_alt PI_2_3_7_tg) (2 * N)
 apply Un_cv_ext with (2 := main).dec3:0 <= / 3 <= 1
dec7:0 <= / 7 <= 1
decr:Un_decreasing PI_2_3_7_tg
cv:Un_cv PI_2_3_7_tg 0
a:-1 <= / 3 <= 1
a0:-1 <= / 7 <= 1
v3:R
Pv3:Un_cv
  (fun N : nat =>
   sum_f_R0 (tg_alt (Ratan_seq (/ 3))) N) v3
v7:R
Pv7:Un_cv
  (fun N : nat =>
   sum_f_R0 (tg_alt (Ratan_seq (/ 7))) N) v7
main:Un_cv
  (fun n : nat =>
   2 * sum_f_R0 (tg_alt (Ratan_seq (/ 3))) n +
   sum_f_R0 (tg_alt (Ratan_seq (/ 7))) n)
  (2 * v3 + v7)
forall n : nat,
2 * sum_f_R0 (tg_alt (Ratan_seq (/ 3))) n +
sum_f_R0 (tg_alt (Ratan_seq (/ 7))) n =
sum_f_R0 (tg_alt PI_2_3_7_tg) n
dec3:0 <= / 3 <= 1
dec7:0 <= / 7 <= 1
decr:Un_decreasing PI_2_3_7_tg
cv:Un_cv PI_2_3_7_tg 0
a:-1 <= / 3 <= 1
a0:-1 <= / 7 <= 1
v3:R
Pv3:Un_cv
  (fun N : nat =>
   sum_f_R0 (tg_alt (Ratan_seq (/ 3))) N) v3
v7:R
Pv7:Un_cv
  (fun N : nat =>
   sum_f_R0 (tg_alt (Ratan_seq (/ 7))) N) v7
main:Un_cv (sum_f_R0 (tg_alt PI_2_3_7_tg))
  (2 * v3 + v7)
forall N : nat,
sum_f_R0 (tg_alt PI_2_3_7_tg) (S (2 * N)) <=
2 * v3 + v7 <= sum_f_R0 (tg_alt PI_2_3_7_tg) (2 * N)
 intros n; rewrite scal_sum, <- plus_sum; apply sum_eq; intros.dec3:0 <= / 3 <= 1
dec7:0 <= / 7 <= 1
decr:Un_decreasing PI_2_3_7_tg
cv:Un_cv PI_2_3_7_tg 0
a:-1 <= / 3 <= 1
a0:-1 <= / 7 <= 1
v3:R
Pv3:Un_cv
  (fun N : nat =>
   sum_f_R0 (tg_alt (Ratan_seq (/ 3))) N) v3
v7:R
Pv7:Un_cv
  (fun N : nat =>
   sum_f_R0 (tg_alt (Ratan_seq (/ 7))) N) v7
main:Un_cv
  (fun n0 : nat =>
   2 * sum_f_R0 (tg_alt (Ratan_seq (/ 3))) n0 +
   sum_f_R0 (tg_alt (Ratan_seq (/ 7))) n0)
  (2 * v3 + v7)
n, i:nat
H:(i <= n)%nat
tg_alt (Ratan_seq (/ 3)) i * 2 +
tg_alt (Ratan_seq (/ 7)) i = 
tg_alt PI_2_3_7_tg i
dec3:0 <= / 3 <= 1
dec7:0 <= / 7 <= 1
decr:Un_decreasing PI_2_3_7_tg
cv:Un_cv PI_2_3_7_tg 0
a:-1 <= / 3 <= 1
a0:-1 <= / 7 <= 1
v3:R
Pv3:Un_cv
  (fun N : nat =>
   sum_f_R0 (tg_alt (Ratan_seq (/ 3))) N) v3
v7:R
Pv7:Un_cv
  (fun N : nat =>
   sum_f_R0 (tg_alt (Ratan_seq (/ 7))) N) v7
main:Un_cv (sum_f_R0 (tg_alt PI_2_3_7_tg))
  (2 * v3 + v7)
forall N : nat,
sum_f_R0 (tg_alt PI_2_3_7_tg) (S (2 * N)) <=
2 * v3 + v7 <= sum_f_R0 (tg_alt PI_2_3_7_tg) (2 * N)
 rewrite Rmult_comm; unfold PI_2_3_7_tg, tg_alt; field.dec3:0 <= / 3 <= 1
dec7:0 <= / 7 <= 1
decr:Un_decreasing PI_2_3_7_tg
cv:Un_cv PI_2_3_7_tg 0
a:-1 <= / 3 <= 1
a0:-1 <= / 7 <= 1
v3:R
Pv3:Un_cv
  (fun N : nat =>
   sum_f_R0 (tg_alt (Ratan_seq (/ 3))) N) v3
v7:R
Pv7:Un_cv
  (fun N : nat =>
   sum_f_R0 (tg_alt (Ratan_seq (/ 7))) N) v7
main:Un_cv (sum_f_R0 (tg_alt PI_2_3_7_tg))
  (2 * v3 + v7)
forall N : nat,
sum_f_R0 (tg_alt PI_2_3_7_tg) (S (2 * N)) <=
2 * v3 + v7 <= sum_f_R0 (tg_alt PI_2_3_7_tg) (2 * N)
intros N; apply (alternated_series_ineq _ _ _ decr cv main).
Qed.