4 files changed, 13 insertions, 13 deletions

diff --git a/theories/Reals/Cos_rel.v b/theories/Reals/Cos_rel.v
index f1675e8d51..f1275c3dbd 100644
--- a/theories/Reals/Cos_rel.v
+++ b/theories/Reals/Cos_rel.v
@@ -271,7 +271,7 @@ Case (exist_cos (Rsqr x)).
 Unfold Rsqr; Intros. 
 Unfold cos_in in p_i. 
 Unfold cos_in in c. 
-Apply unicite_sum with [i:nat]``(cos_n i)*(pow (x*x) i)``; Assumption. 
+Apply unicity_sum with [i:nat]``(cos_n i)*(pow (x*x) i)``; Assumption. 
 Qed. 
  
 Lemma C1_cvg : (x,y:R) (Un_cv (C1 x y) (cos (Rplus x y))). 
@@ -301,7 +301,7 @@ Case (exist_cos (Rsqr ``x+y``)).
 Unfold Rsqr; Intros. 
 Unfold cos_in in p_i. 
 Unfold cos_in in c. 
-Apply unicite_sum with [i:nat]``(cos_n i)*(pow ((x+y)*(x+y)) i)``; Assumption. 
+Apply unicity_sum with [i:nat]``(cos_n i)*(pow ((x+y)*(x+y)) i)``; Assumption. 
 Qed. 
  
 Lemma B1_cvg : (x:R) (Un_cv (B1 x) (sin x)). 
@@ -353,6 +353,6 @@ Case (exist_sin (Rsqr x)).
 Unfold Rsqr; Intros. 
 Unfold sin_in in p_i. 
 Unfold sin_in in s. 
-Assert H1 := (unicite_sum [i:nat]``(sin_n i)*(pow (x*x) i)`` x0 x1 p_i s). 
+Assert H1 := (unicity_sum [i:nat]``(sin_n i)*(pow (x*x) i)`` x0 x1 p_i s). 
 Rewrite H1; Reflexivity. 
 Qed. 
diff --git a/theories/Reals/PartSum.v b/theories/Reals/PartSum.v
index a072485081..cddcf54c16 100644
--- a/theories/Reals/PartSum.v
+++ b/theories/Reals/PartSum.v
@@ -22,7 +22,7 @@ Apply HrecN; Intros; Apply H; Apply le_S; Assumption.
 Apply H; Apply le_n.
 Qed.
 
-(* Relation de Chasles *)
+(* Chasles' relation *)
 Lemma tech2 : (An:nat->R;m,n:nat) (lt m n) -> (sum_f_R0 An n) == (Rplus (sum_f_R0 An m) (sum_f_R0 [i:nat]``(An (plus (S m) i))`` (minus n (S m)))). 
 Intros; Induction n.
 Elim (lt_n_O ? H).
@@ -48,7 +48,7 @@ Right; Reflexivity.
 Left; Apply lt_le_trans with (S m); [Apply lt_n_Sn | Assumption].
 Qed.
 
-(* Somme d'une suite géométrique *)
+(* Sum of geometric sequences *)
 Lemma tech3 : (k:R;N:nat) ``k<>1`` -> (sum_f_R0 [i:nat](pow k i) N)==``(1-(pow k (S N)))/(1-k)``.
 Intros; Cut ``1-k<>0``.
 Intro; Induction N.
@@ -154,8 +154,8 @@ Rewrite (H (S N)); [Reflexivity | Apply le_n].
 Intros; Apply H; Apply le_trans with N; [Assumption | Apply le_n_Sn].
 Qed.
 
-(* Unicité de la limite d'une série convergente *)
-Lemma unicite_sum : (An:nat->R;l1,l2:R) (infinit_sum An l1) -> (infinit_sum An l2) -> l1 == l2.
+(* Unicity of the limit defined by convergent series *)
+Lemma unicity_sum : (An:nat->R;l1,l2:R) (infinit_sum An l1) -> (infinit_sum An l2) -> l1 == l2.
 Unfold infinit_sum; Intros.
 Case (Req_EM l1 l2); Intro.
 Assumption.
@@ -276,10 +276,10 @@ Apply HrecN.
 Apply H.
 Qed.
 
-(* Le critère de Cauchy pour les séries *)
+(* Cauchy's criterion for series *)
 Definition Cauchy_crit_series [An:nat->R] : Prop := (Cauchy_crit [N:nat](sum_f_R0 An N)).
 
-(* Si (|An|) verifie le critere de Cauchy pour les séries , alors (An) aussi *)
+(* If (|An|) satisfies the Cauchy's criterion for series, then (An) too *)
 Lemma cauchy_abs : (An:nat->R) (Cauchy_crit_series [i:nat](Rabsolu (An i))) -> (Cauchy_crit_series An).
 Unfold Cauchy_crit_series; Unfold Cauchy_crit.
 Intros.
diff --git a/theories/Reals/Rtrigo_alt.v b/theories/Reals/Rtrigo_alt.v
index 37a9080372..99d6a736ba 100644
--- a/theories/Reals/Rtrigo_alt.v
+++ b/theories/Reals/Rtrigo_alt.v
@@ -129,7 +129,7 @@ Unfold sin; Case (exist_sin (Rsqr a)).
 Intros; Cut x==x0.
 Intro; Rewrite H3; Unfold Rdiv.
 Symmetry; Apply Rinv_r_simpl_m; Assumption.
-Unfold sin_in in p; Unfold sin_in in s; EApply unicite_sum.
+Unfold sin_in in p; Unfold sin_in in s; EApply unicity_sum.
 Apply p.
 Apply s.
 Intros; Elim H2; Intros.
@@ -251,7 +251,7 @@ Rewrite pow_Rsqr; Reflexivity.
 Simpl; Ring.
 Unfold cos_n; Unfold Rdiv; Simpl; Rewrite Rinv_R1; Rewrite Rmult_1r; Reflexivity.
 Apply lt_O_Sn.
-Unfold cos; Case (exist_cos (Rsqr a0)); Intros; Unfold cos_in in p; Unfold cos_in in c; EApply unicite_sum.
+Unfold cos; Case (exist_cos (Rsqr a0)); Intros; Unfold cos_in in p; Unfold cos_in in c; EApply unicity_sum.
 Apply p.
 Apply c.
 Intros; Elim H3; Intros; Replace ``(cos a0)-1`` with ``-(1-(cos a0))``; [Idtac | Ring].
diff --git a/theories/Reals/Rtrigo_def.v b/theories/Reals/Rtrigo_def.v
index fdeefb6f3c..038f1efb77 100644
--- a/theories/Reals/Rtrigo_def.v
+++ b/theories/Reals/Rtrigo_def.v
@@ -57,7 +57,7 @@ Defined.
 Lemma exp_0 : ``(exp 0)==1``. 
 Cut (exp_in R0 (exp R0)).
 Cut (exp_in R0 R1).
-Unfold exp_in; Intros; EApply unicite_sum.
+Unfold exp_in; Intros; EApply unicity_sum.
 Apply H0.
 Apply H.
 Exact (projT2 ? ? exist_exp0).
@@ -350,7 +350,7 @@ Defined.
 Lemma cos_0 : ``(cos 0)==1``.
 Cut (cos_in R0 (cos R0)).
 Cut (cos_in R0 R1).
-Unfold cos_in; Intros; EApply unicite_sum.
+Unfold cos_in; Intros; EApply unicity_sum.
 Apply H0.
 Apply H.
 Exact (projT2 ? ? exist_cos0).