From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Sun, 25 Jan 2015 14:42:51 +0100
Subject: Imported Upstream version 8.5~beta1+dfsg

---
 theories/Reals/Machin.v | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

(limited to 'theories/Reals/Machin.v')

diff --git a/theories/Reals/Machin.v b/theories/Reals/Machin.v
index 40a857e3..1a94f6a8 100644
--- a/theories/Reals/Machin.v
+++ b/theories/Reals/Machin.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -16,6 +16,7 @@ Require Import Rseries.
 Require Import SeqProp.
 Require Import PartSum.
 Require Import Ratan.
+Require Import Omega.
 
 Local Open Scope R_scope.
 
@@ -27,6 +28,7 @@ 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).
+Proof.
 intros u v pn0 uvint aint.
 assert (cos (atan u) <> 0).
  destruct (atan_bound u); apply Rgt_not_eq, cos_gt_0; auto.
@@ -44,6 +46,7 @@ Qed.
 
 Lemma tech : forall x y , -1 <= x <= 1 -> -1 < y < 1 -> 
   -PI/2 < atan x - atan y < PI/2.
+Proof.
 assert (ut := PI_RGT_0).
 intros x y [xm1 x1] [ym1 y1].
 assert (-(PI/4) <= atan x).
@@ -67,6 +70,7 @@ Qed.
 
 (* A simple formula, reasonably efficient. *)
 Lemma Machin_2_3 : PI/4 = atan(/2) + atan(/3).
+Proof.
 assert (utility : 0 < PI/2) by (apply PI2_RGT_0).
 rewrite <- atan_1.
 rewrite (atan_sub_correct 1 (/2)).
@@ -77,6 +81,7 @@ apply atan_bound.
 Qed.
 
 Lemma Machin_4_5_239 : PI/4 = 4 * atan (/5) - atan(/239).
+Proof.
 rewrite <- atan_1.
 rewrite (atan_sub_correct 1 (/5));
  [ | apply Rgt_not_eq; fourier | apply tech; try split; fourier |
@@ -105,6 +110,7 @@ unfold atan_sub; field.
 Qed.
 
 Lemma Machin_2_3_7 : PI/4 = 2 * atan(/3) + (atan (/7)).
+Proof.
 rewrite <- atan_1.
 rewrite (atan_sub_correct 1 (/3));
  [ | apply Rgt_not_eq; fourier | apply tech; try split; fourier |
-- 
cgit v1.2.3