Une passe sur les réels:

- Renommage de Rlt_not_le de Fourier_util en Rlt_not_le_frac_opp pour
  éviter la confusion avec le Rlt_not_le de RIneq.
- Quelques variantes de lemmes en plus dans RIneq.
- Déplacement des énoncés de sigT dans sig (y compris la complétude)
  et utilisation de la notation { l:R | }.
- Suppression hypothèse inutile de ln_exists1.
- Ajout notation ² pour Rsqr.

Au passage:
- Déplacement de dec_inh_nat_subset_has_unique_least_element
  de ChoiceFacts vers Wf_nat.
- Correction de l'espace en trop dans les notations de Specif.v liées à "&".
- MAJ fichier CHANGES

Note: il reste un axiome dans Ranalysis (raison technique: Ltac ne
sait pas manipuler un terme ouvert) et dans Rtrigo.v ("sin PI/2 = 1"
non prouvé).



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10710 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 9 insertions, 5 deletions

diff --git a/theories/Reals/Rlogic.v b/theories/Reals/Rlogic.v
index e10c3ab40..b8c85458c 100644
--- a/theories/Reals/Rlogic.v
+++ b/theories/Reals/Rlogic.v
@@ -6,10 +6,11 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(** This module proves the decidablity of arithmetical statements from
-the axiom that the order of the real numbers is decidable. *)
+(** * This module proves the decidablity of arithmetical statements from
+excluded middle and the axiom that the order of the real numbers is
+decidable. *)
 
-(** Assuming a decidable predicate [P n], A series is constructed who's
+(** Assuming a decidable predicate [P n], A series is constructed whose
 [n]th term is 1/2^n if [P n] holds and 0 otherwise.  This sum reaches 2
 only if [P n] holds for all [n], otherwise the sum is less than 2.
 Comparing the sum to 2 decides if [forall n, P n] or [~forall n, P n] *)
@@ -20,7 +21,10 @@ statement in the arithmetical hierarchy. *)
 (** Contributed by Cezary Kaliszyk and Russell O'Connor *)
 
 Require Import ConstructiveEpsilon.
-Require Import Reals.
+Require Import Rfunctions.
+Require Import PartSum.
+Require Import SeqSeries.
+Require Import RiemannInt.
 Require Import Fourier.
  
 Section Arithmetical_dec.
@@ -130,7 +134,7 @@ assert (A0:=(GP_infinite (1/2) A)).
 symmetry.
  split; intro.
  replace 2 with (/ (1 - (1 / 2))) by field.
- unfold Pser, infinit_sum in A0.
+ unfold Pser, infinite_sum in A0.
  eapply Rle_cv_lim;[|unfold Un_cv; apply A0 |apply u].
  intros n.
  clear -n H.