From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 29 Dec 2018 14:31:27 -0500
Subject: Imported Upstream version 8.8.2

---
 theories/Reals/Rtrigo_alt.v | 79 +++++++++++++++++++++------------------------
 1 file changed, 36 insertions(+), 43 deletions(-)

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

diff --git a/theories/Reals/Rtrigo_alt.v b/theories/Reals/Rtrigo_alt.v
index a5092d22..71b90fb4 100644
--- a/theories/Reals/Rtrigo_alt.v
+++ b/theories/Reals/Rtrigo_alt.v
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   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        *)
+(*    //   *    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 Rbase.
@@ -99,24 +101,22 @@ Proof.
   apply Rle_trans with 20.
   apply Rle_trans with 16.
   replace 16 with (Rsqr 4); [ idtac | ring_Rsqr ].
-  replace (a * a) with (Rsqr a); [ idtac | reflexivity ].
   apply Rsqr_incr_1.
   assumption.
   assumption.
-  left; prove_sup0.
-  rewrite <- (Rplus_0_r 16); replace 20 with (16 + 4);
-    [ apply Rplus_le_compat_l; left; prove_sup0 | ring ].
-  rewrite <- (Rplus_comm 20); pattern 20 at 1; rewrite <- Rplus_0_r;
-    apply Rplus_le_compat_l.
+  now apply IZR_le.
+  now apply IZR_le.
+  rewrite <- (Rplus_0_l 20) at 1;
+    apply Rplus_le_compat_r.
   apply Rplus_le_le_0_compat.
-  repeat apply Rmult_le_pos.
-  left; prove_sup0.
-  left; prove_sup0.
-  replace 0 with (INR 0); [ apply le_INR; apply le_O_n | reflexivity ].
-  replace 0 with (INR 0); [ apply le_INR; apply le_O_n | reflexivity ].
   apply Rmult_le_pos.
-  left; prove_sup0.
-  replace 0 with (INR 0); [ apply le_INR; apply le_O_n | reflexivity ].
+  apply Rmult_le_pos.
+  now apply IZR_le.
+  apply pos_INR.
+  apply pos_INR.
+  apply Rmult_le_pos.
+  now apply IZR_le.
+  apply pos_INR.
   apply INR_fact_neq_0.
   apply INR_fact_neq_0.
   simpl; ring.
@@ -182,16 +182,14 @@ Proof.
   replace (- sum_f_R0 (tg_alt Un) (S (2 * n))) with
   (-1 * sum_f_R0 (tg_alt Un) (S (2 * n))); [ rewrite scal_sum | ring ].
   apply sum_eq; intros; unfold sin_term, Un, tg_alt;
-    replace ((-1) ^ S i) with (-1 * (-1) ^ i).
+    change ((-1) ^ S i) with (-1 * (-1) ^ i).
   unfold Rdiv; ring.
-  reflexivity.
   replace (- sum_f_R0 (tg_alt Un) (2 * n)) with
   (-1 * sum_f_R0 (tg_alt Un) (2 * n)); [ rewrite scal_sum | ring ].
   apply sum_eq; intros.
   unfold sin_term, Un, tg_alt;
-    replace ((-1) ^ S i) with (-1 * (-1) ^ i).
+    change ((-1) ^ S i) with (-1 * (-1) ^ i).
   unfold Rdiv; ring.
-  reflexivity.
   replace (2 * (n + 1))%nat with (S (S (2 * n))).
   reflexivity.
   ring.
@@ -279,26 +277,23 @@ Proof.
     with (4 * INR n1 * INR n1 + 14 * INR n1 + 12); [ idtac | ring ].
   apply Rle_trans with 12.
   apply Rle_trans with 4.
-  replace 4 with (Rsqr 2); [ idtac | ring_Rsqr ].
-  replace (a0 * a0) with (Rsqr a0); [ idtac | reflexivity ].
+  change 4 with (Rsqr 2).
   apply Rsqr_incr_1.
   assumption.
-  discrR.
   assumption.
-  left; prove_sup0.
-  pattern 4 at 1; rewrite <- Rplus_0_r; replace 12 with (4 + 8);
-    [ apply Rplus_le_compat_l; left; prove_sup0 | ring ].
-  rewrite <- (Rplus_comm 12); pattern 12 at 1; rewrite <- Rplus_0_r;
-    apply Rplus_le_compat_l.
+  now apply IZR_le.
+  now apply IZR_le.
+  rewrite <- (Rplus_0_l 12) at 1;
+    apply Rplus_le_compat_r.
   apply Rplus_le_le_0_compat.
-  repeat apply Rmult_le_pos.
-  left; prove_sup0.
-  left; prove_sup0.
-  replace 0 with (INR 0); [ apply le_INR; apply le_O_n | reflexivity ].
-  replace 0 with (INR 0); [ apply le_INR; apply le_O_n | reflexivity ].
   apply Rmult_le_pos.
-  left; prove_sup0.
-  replace 0 with (INR 0); [ apply le_INR; apply le_O_n | reflexivity ].
+  apply Rmult_le_pos.
+  now apply IZR_le.
+  apply pos_INR.
+  apply pos_INR.
+  apply Rmult_le_pos.
+  now apply IZR_le.
+  apply pos_INR.
   apply INR_fact_neq_0.
   apply INR_fact_neq_0.
   simpl; ring.
@@ -320,7 +315,7 @@ Proof.
   (1 - sum_f_R0 (fun i:nat => cos_n i * Rsqr a0 ^ i) (S n1)).
   unfold Rminus; rewrite Ropp_plus_distr; rewrite Ropp_involutive;
     repeat rewrite Rplus_assoc; rewrite (Rplus_comm 1);
-      rewrite (Rplus_comm (-1)); repeat rewrite Rplus_assoc;
+      rewrite (Rplus_comm (-(1))); repeat rewrite Rplus_assoc;
         rewrite Rplus_opp_l; rewrite Rplus_0_r; rewrite <- Rabs_Ropp;
           rewrite Ropp_plus_distr; rewrite Ropp_involutive;
             unfold Rminus in H6; apply H6.
@@ -351,15 +346,13 @@ Proof.
   replace (- sum_f_R0 (tg_alt Un) (S (2 * n0))) with
   (-1 * sum_f_R0 (tg_alt Un) (S (2 * n0))); [ rewrite scal_sum | ring ].
   apply sum_eq; intros; unfold cos_term, Un, tg_alt;
-    replace ((-1) ^ S i) with (-1 * (-1) ^ i).
+    change ((-1) ^ S i) with (-1 * (-1) ^ i).
   unfold Rdiv; ring.
-  reflexivity.
   replace (- sum_f_R0 (tg_alt Un) (2 * n0)) with
   (-1 * sum_f_R0 (tg_alt Un) (2 * n0)); [ rewrite scal_sum | ring ];
   apply sum_eq; intros; unfold cos_term, Un, tg_alt;
-    replace ((-1) ^ S i) with (-1 * (-1) ^ i).
+    change ((-1) ^ S i) with (-1 * (-1) ^ i).
   unfold Rdiv; ring.
-  reflexivity.
   replace (2 * (n0 + 1))%nat with (S (S (2 * n0))).
   reflexivity.
   ring.
@@ -367,10 +360,10 @@ Proof.
   reflexivity.
   ring.
   intro; elim H2; intros; split.
-  apply Rplus_le_reg_l with (-1).
+  apply Rplus_le_reg_l with (-(1)).
   rewrite <- Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_l;
     rewrite (Rplus_comm (-1)); apply H3.
-  apply Rplus_le_reg_l with (-1).
+  apply Rplus_le_reg_l with (-(1)).
   rewrite <- Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_l;
     rewrite (Rplus_comm (-1)); apply H4.
   unfold cos_term; simpl; unfold Rdiv; rewrite Rinv_1;
-- 
cgit v1.2.3