Add some missing Proof keywords.

4 files changed, 22 insertions, 0 deletions

diff --git a/theories/Reals/Alembert.v b/theories/Reals/Alembert.v
index e848e4df8..011328ec0 100644
--- a/theories/Reals/Alembert.v
+++ b/theories/Reals/Alembert.v
@@ -572,6 +572,7 @@ Lemma Alembert_C6 :
     (forall n:nat, An n <> 0) ->
     Un_cv (fun n:nat => Rabs (An (S n) / An n)) k ->
     Rabs x < / k -> { l:R | Pser An x l }.
+Proof.
   intros.
   cut { l:R | Un_cv (fun N:nat => sum_f_R0 (fun i:nat => An i * x ^ i) N) l }.
   intro X.
diff --git a/theories/Reals/Cos_rel.v b/theories/Reals/Cos_rel.v
index f5b34de9c..cfb30662b 100644
--- a/theories/Reals/Cos_rel.v
+++ b/theories/Reals/Cos_rel.v
@@ -50,6 +50,7 @@ Theorem cos_plus_form :
  forall (x y:R) (n:nat),
    (0 < n)%nat ->
    A1 x (S n) * A1 y (S n) - B1 x n * B1 y n + Reste x y n = C1 x y (S n).
+Proof.
 intros.
 unfold A1, B1.
 rewrite
@@ -251,12 +252,14 @@ apply lt_O_Sn.
 Qed.
 
 Lemma pow_sqr : forall (x:R) (i:nat), x ^ (2 * i) = (x * x) ^ i.
+Proof.
 intros.
 assert (H := pow_Rsqr x i).
 unfold Rsqr in H; exact H.
 Qed.
 
 Lemma A1_cvg : forall x:R, Un_cv (A1 x) (cos x).
+Proof.
 intro.
 unfold cos; destruct (exist_cos (Rsqr x)) as (x0,p).
 unfold cos_in, cos_n, infinite_sum, R_dist in p.
@@ -276,6 +279,7 @@ apply pow_sqr.
 Qed.
 
 Lemma C1_cvg : forall x y:R, Un_cv (C1 x y) (cos (x + y)).
+Proof.
 intros.
 unfold cos.
 destruct (exist_cos (Rsqr (x + y))) as (x0,p).
@@ -298,6 +302,7 @@ apply pow_sqr.
 Qed.
 
 Lemma B1_cvg : forall x:R, Un_cv (B1 x) (sin x).
+Proof.
 intro.
 case (Req_dec x 0); intro.
 rewrite H.
diff --git a/theories/Reals/PSeries_reg.v b/theories/Reals/PSeries_reg.v
index 30a26f770..94b881ccc 100644
--- a/theories/Reals/PSeries_reg.v
+++ b/theories/Reals/PSeries_reg.v
@@ -24,6 +24,7 @@ Definition Boule (x:R) (r:posreal) (y:R) : Prop := Rabs (y - x) < r.
 
 Lemma Boule_convex : forall c d x y z,
   Boule c d x -> Boule c d y -> x <= z <= y -> Boule c d z.
+Proof.
 intros c d x y z bx b_y intz.
 unfold Boule in bx, b_y; apply Rabs_def2 in bx;
 apply Rabs_def2 in b_y; apply Rabs_def1;
@@ -33,6 +34,7 @@ Qed.
 
 Definition boule_of_interval x y (h : x < y) :
   {c :R & {r : posreal | c - r = x /\ c + r = y}}.
+Proof.
 exists ((x + y)/2).
 assert (radius : 0 < (y - x)/2).
  unfold Rdiv; apply Rmult_lt_0_compat.
@@ -71,6 +73,7 @@ Qed.
 Lemma Ball_in_inter : forall c1 c2 r1 r2 x,
   Boule c1 r1 x -> Boule c2 r2 x ->
   {r3 : posreal | forall y, Boule x r3 y -> Boule c1 r1 y /\ Boule c2 r2 y}.
+Proof.
 intros c1 c2 [r1 r1p] [r2 r2p] x; unfold Boule; simpl; intros in1 in2.
 assert (Rmax (c1 - r1)(c2 - r2) < x).
  apply Rmax_lub_lt;[revert in1 | revert in2]; intros h;
@@ -366,6 +369,7 @@ Qed.
 (* Uniform convergence implies pointwise simple convergence *)
 Lemma CVU_cv : forall f g c d, CVU f g c d ->
    forall x, Boule c d x -> Un_cv (fun n => f n x) (g x).
+Proof.
 intros f g c d cvu x bx eps ep; destruct (cvu eps ep) as [N Pn].
  exists N; intros n nN; rewrite R_dist_sym; apply Pn; assumption.
 Qed.
@@ -374,6 +378,7 @@ Qed.
 Lemma CVU_ext_lim :
   forall f g1 g2 c d, CVU f g1 c d -> (forall x, Boule c d x -> g1 x = g2 x) ->
     CVU f g2 c d.
+Proof.
 intros f g1 g2 c d cvu q eps ep; destruct (cvu _ ep) as [N Pn].
 exists N; intros; rewrite <- q; auto.
 Qed.
@@ -388,6 +393,7 @@ Lemma CVU_derivable :
    (forall x, Boule c d x -> Un_cv (fun n => f n x) (g x)) ->
    (forall n x, Boule c d x -> derivable_pt_lim (f n) x (f' n x)) ->
    forall x, Boule c d x -> derivable_pt_lim g x (g' x).
+Proof.
 intros f f' g g' c d cvu cvp dff' x bx.
 set (rho_ :=
        fun n y =>
diff --git a/theories/Reals/Ratan.v b/theories/Reals/Ratan.v
index 68718db0e..cc45139d2 100644
--- a/theories/Reals/Ratan.v
+++ b/theories/Reals/Ratan.v
@@ -450,6 +450,7 @@ fourier.
 Qed.
 
 Definition frame_tan y : {x | 0 < x < PI/2 /\ Rabs y < tan x}.
+Proof.
 destruct (total_order_T (Rabs y) 1) as [Hs|Hgt].
  assert (yle1 : Rabs y <= 1) by (destruct Hs; fourier).
  clear Hs; exists 1; split;[split; [exact Rlt_0_1 | exact PI2_1] | ].
@@ -567,10 +568,12 @@ Lemma pos_opp_lt : forall x, 0 < x -> -x < x.
 Proof. intros; fourier. Qed.
 
 Lemma tech_opp_tan : forall x y, -tan x < y -> tan (-x) < y.
+Proof.
 intros; rewrite tan_neg; assumption.
 Qed.
 
 Definition pre_atan (y : R) : {x : R | -PI/2 < x < PI/2 /\ tan x = y}.
+Proof.
 destruct (frame_tan y) as [ub [[ub0 ubpi2] Ptan_ub]].
 set (pr := (conj (tech_opp_tan _ _ (proj2 (Rabs_def2 _ _ Ptan_ub)))
      (proj1 (Rabs_def2 _ _ Ptan_ub)))).
@@ -649,6 +652,7 @@ exact df_neq.
 Qed.
 
 Lemma atan_increasing : forall x y, x < y -> atan x < atan y.
+Proof.
 intros x y d.
 assert (t1 := atan_bound x).
 assert (t2 := atan_bound y).
@@ -663,6 +667,7 @@ solve[rewrite yx; apply Rle_refl].
 Qed.
 
 Lemma atan_0 : atan 0 = 0.
+Proof.
 apply tan_is_inj; try (apply atan_bound).
  assert (t := PI_RGT_0); rewrite Ropp_div; split; fourier.
 rewrite atan_right_inv, tan_0.
@@ -670,6 +675,7 @@ reflexivity.
 Qed.
 
 Lemma atan_1 : atan 1 = PI/4.
+Proof.
 assert (ut := PI_RGT_0).
 assert (-PI/2 < PI/4 < PI/2) by (rewrite Ropp_div; split; fourier).
 assert (t := atan_bound 1).
@@ -865,6 +871,7 @@ Qed.
 
 Definition ps_atan_exists_01 (x : R) (Hx:0 <= x <= 1) :
    {l : R | Un_cv (fun N : nat => sum_f_R0 (tg_alt (Ratan_seq x)) N) l}.
+Proof.
 exact (alternated_series (Ratan_seq x)
   (Ratan_seq_decreasing _ Hx) (Ratan_seq_converging _ Hx)).
 Defined.
@@ -888,6 +895,7 @@ Qed.
 
 Definition ps_atan_exists_1 (x : R) (Hx : -1 <= x <= 1) :
    {l : R | Un_cv (fun N : nat => sum_f_R0 (tg_alt (Ratan_seq x)) N) l}.
+Proof.
 destruct (Rle_lt_dec 0 x).
  assert (pr : 0 <= x <= 1) by tauto.
  exact (ps_atan_exists_01 x pr).
@@ -902,6 +910,7 @@ solve[intros; exists 0%nat; intros; rewrite R_dist_eq; auto].
 Qed.
 
 Definition in_int (x : R) : {-1 <= x <= 1}+{~ -1 <= x <= 1}.
+Proof.
 destruct (Rle_lt_dec x 1).
  destruct (Rle_lt_dec (-1) x).
   left;split; auto.
@@ -1563,6 +1572,7 @@ Qed.
 
 
 Theorem Alt_PI_eq : Alt_PI = PI.
+Proof.
 apply Rmult_eq_reg_r with (/4); fold (Alt_PI/4); fold (PI/4);
   [ | apply Rgt_not_eq; fourier].
 assert (0 < PI/6) by (apply PI6_RGT_0).