aboutsummaryrefslogtreecommitdiff
path: root/theories/Reals
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Reals')
-rw-r--r--theories/Reals/Alembert.v8
-rw-r--r--theories/Reals/AltSeries.v2
-rw-r--r--theories/Reals/ArithProp.v6
-rw-r--r--theories/Reals/Binomial.v8
-rw-r--r--theories/Reals/Cauchy_prod.v4
-rw-r--r--theories/Reals/Cos_plus.v14
-rw-r--r--theories/Reals/Cos_rel.v4
-rw-r--r--theories/Reals/Exp_prop.v6
-rw-r--r--theories/Reals/MVT.v4
-rw-r--r--theories/Reals/NewtonInt.v8
-rw-r--r--theories/Reals/PSeries_reg.v4
-rw-r--r--theories/Reals/PartSum.v12
-rw-r--r--theories/Reals/Ranalysis1.v2
-rw-r--r--theories/Reals/Rcomplete.v6
-rw-r--r--theories/Reals/RiemannInt.v76
-rw-r--r--theories/Reals/RiemannInt_SF.v14
-rw-r--r--theories/Reals/Rpower.v4
-rw-r--r--theories/Reals/Rsqrt_def.v8
-rw-r--r--theories/Reals/Rtopology.v82
-rw-r--r--theories/Reals/Rtrigo.v4
-rw-r--r--theories/Reals/Rtrigo_alt.v4
-rw-r--r--theories/Reals/Rtrigo_reg.v10
-rw-r--r--theories/Reals/SeqProp.v20
-rw-r--r--theories/Reals/SeqSeries.v8
-rw-r--r--theories/Reals/Sqrt_reg.v8
25 files changed, 163 insertions, 163 deletions
diff --git a/theories/Reals/Alembert.v b/theories/Reals/Alembert.v
index 7d8a939143..396029c035 100644
--- a/theories/Reals/Alembert.v
+++ b/theories/Reals/Alembert.v
@@ -121,8 +121,8 @@ Lemma Alembert_C2 :
Un_cv (fun n:nat => Rabs (An (S n) / An n)) 0 ->
sigT (fun l:R => Un_cv (fun N:nat => sum_f_R0 An N) l).
intros.
-pose (Vn := fun i:nat => (2 * Rabs (An i) + An i) / 2).
-pose (Wn := fun i:nat => (2 * Rabs (An i) - An i) / 2).
+set (Vn := fun i:nat => (2 * Rabs (An i) + An i) / 2).
+set (Wn := fun i:nat => (2 * Rabs (An i) - An i) / 2).
cut (forall n:nat, 0 < Vn n).
intro; cut (forall n:nat, 0 < Wn n).
intro; cut (Un_cv (fun n:nat => Rabs (Vn (S n) / Vn n)) 0).
@@ -135,7 +135,7 @@ apply existT with (x - x0); unfold Un_cv in |- *; unfold Un_cv in p;
unfold Un_cv in p0; intros; cut (0 < eps / 2).
intro; elim (p (eps / 2) H8); clear p; intros.
elim (p0 (eps / 2) H8); clear p0; intros.
-pose (N := max x1 x2).
+set (N := max x1 x2).
exists N; intros;
replace (sum_f_R0 An n) with (sum_f_R0 Vn n - sum_f_R0 Wn n).
unfold R_dist in |- *;
@@ -340,7 +340,7 @@ Lemma AlembertC3_step1 :
(forall n:nat, An n <> 0) ->
Un_cv (fun n:nat => Rabs (An (S n) / An n)) 0 ->
sigT (fun l:R => Pser An x l).
-intros; pose (Bn := fun i:nat => An i * x ^ i).
+intros; set (Bn := fun i:nat => An i * x ^ i).
cut (forall n:nat, Bn n <> 0).
intro; cut (Un_cv (fun n:nat => Rabs (Bn (S n) / Bn n)) 0).
intro; assert (H4 := Alembert_C2 Bn H2 H3).
diff --git a/theories/Reals/AltSeries.v b/theories/Reals/AltSeries.v
index e9be3fc028..9cbbd1ea5d 100644
--- a/theories/Reals/AltSeries.v
+++ b/theories/Reals/AltSeries.v
@@ -164,7 +164,7 @@ intros; cut (0 < eps / 2);
[ assumption | apply Rinv_0_lt_compat; prove_sup0 ] ].
elim (H1 (eps / 2) H5); intros N2 H6.
elim (p (eps / 2) H5); intros N1 H7.
-pose (N := max (S (2 * N1)) N2).
+set (N := max (S (2 * N1)) N2).
exists N; intros.
assert (H9 := even_odd_cor n).
elim H9; intros P H10.
diff --git a/theories/Reals/ArithProp.v b/theories/Reals/ArithProp.v
index 8be8c47faf..ef632a0914 100644
--- a/theories/Reals/ArithProp.v
+++ b/theories/Reals/ArithProp.v
@@ -20,7 +20,7 @@ intros; red in |- *; intro.
cut (forall n m:nat, (m <= n)%nat -> (n - m)%nat = 0%nat -> n = m).
intro; assert (H2 := H1 _ _ (lt_le_weak _ _ H) H0); rewrite H2 in H;
elim (lt_irrefl _ H).
-pose (R := fun n m:nat => (m <= n)%nat -> (n - m)%nat = 0%nat -> n = m).
+set (R := fun n m:nat => (m <= n)%nat -> (n - m)%nat = 0%nat -> n = m).
cut
((forall n m:nat, R n m) ->
forall n0 m:nat, (m <= n0)%nat -> (n0 - m)%nat = 0%nat -> n0 = m).
@@ -34,7 +34,7 @@ unfold R in |- *; intros; apply H1; assumption.
Qed.
Lemma le_minusni_n : forall n i:nat, (i <= n)%nat -> (n - i <= n)%nat.
-pose (R := fun m n:nat => (n <= m)%nat -> (m - n <= m)%nat).
+set (R := fun m n:nat => (n <= m)%nat -> (m - n <= m)%nat).
cut
((forall m n:nat, R m n) -> forall n i:nat, (i <= n)%nat -> (n - i <= n)%nat).
intro; apply H.
@@ -89,7 +89,7 @@ Lemma euclidian_division :
y <> 0 ->
exists k : Z, (exists r : R, x = IZR k * y + r /\ 0 <= r < Rabs y).
intros.
-pose
+set
(k0 :=
match Rcase_abs y with
| left _ => (1 - up (x / - y))%Z
diff --git a/theories/Reals/Binomial.v b/theories/Reals/Binomial.v
index e8173b82e4..ad5a358e8a 100644
--- a/theories/Reals/Binomial.v
+++ b/theories/Reals/Binomial.v
@@ -135,7 +135,7 @@ replace (y ^ 0) with 1; [ rewrite Rmult_1_r | simpl in |- *; reflexivity ].
induction n as [| n Hrecn0].
simpl in |- *; do 2 rewrite H; ring.
(* N >= 1 *)
-pose (N := S n).
+set (N := S n).
rewrite Rmult_plus_distr_l.
replace (sum_f_R0 (fun i:nat => C N i * x ^ i * y ^ (N - i)) N * x) with
(sum_f_R0 (fun i:nat => C N i * x ^ S i * y ^ (N - i)) N).
@@ -145,8 +145,8 @@ rewrite (decomp_sum (fun i:nat => C (S N) i * x ^ i * y ^ (S N - i)) N).
rewrite H; replace (x ^ 0) with 1; [ idtac | reflexivity ].
do 2 rewrite Rmult_1_l.
replace (S N - 0)%nat with (S N); [ idtac | reflexivity ].
-pose (An := fun i:nat => C N i * x ^ S i * y ^ (N - i)).
-pose (Bn := fun i:nat => C N (S i) * x ^ S i * y ^ (N - i)).
+set (An := fun i:nat => C N i * x ^ S i * y ^ (N - i)).
+set (Bn := fun i:nat => C N (S i) * x ^ S i * y ^ (N - i)).
replace (pred N) with n.
replace (sum_f_R0 (fun i:nat => C (S N) (S i) * x ^ S i * y ^ (S N - S i)) n)
with (sum_f_R0 (fun i:nat => An i + Bn i) n).
@@ -156,7 +156,7 @@ rewrite (Rplus_comm (sum_f_R0 An n)).
repeat rewrite Rplus_assoc.
rewrite <- tech5.
fold N in |- *.
-pose (Cn := fun i:nat => C N i * x ^ i * y ^ (S N - i)).
+set (Cn := fun i:nat => C N i * x ^ i * y ^ (S N - i)).
cut (forall i:nat, (i < N)%nat -> Cn (S i) = Bn i).
intro; replace (sum_f_R0 Bn n) with (sum_f_R0 (fun i:nat => Cn (S i)) n).
replace (y ^ S N) with (Cn 0%nat).
diff --git a/theories/Reals/Cauchy_prod.v b/theories/Reals/Cauchy_prod.v
index 6cd5fa17fa..543e1a8520 100644
--- a/theories/Reals/Cauchy_prod.v
+++ b/theories/Reals/Cauchy_prod.v
@@ -115,13 +115,13 @@ replace
(pred (pred (N - k)))) (pred (pred N)) +
An (S N) * sum_f_R0 (fun l:nat => Bn (S l)) (pred N)).
rewrite (decomp_sum Bn N H1); rewrite Rmult_plus_distr_l.
-pose
+set
(Z :=
sum_f_R0
(fun k:nat =>
sum_f_R0 (fun l:nat => An (S (S (l + k))) * Bn (N - l)%nat)
(pred (pred (N - k)))) (pred (pred N)));
- pose (Z2 := sum_f_R0 (fun i:nat => Bn (S i)) (pred N));
+ set (Z2 := sum_f_R0 (fun i:nat => Bn (S i)) (pred N));
ring.
rewrite
(sum_N_predN
diff --git a/theories/Reals/Cos_plus.v b/theories/Reals/Cos_plus.v
index d29193ad7d..f2b2bcd850 100644
--- a/theories/Reals/Cos_plus.v
+++ b/theories/Reals/Cos_plus.v
@@ -20,8 +20,8 @@ Definition Majxy (x y:R) (n:nat) : R :=
Lemma Majxy_cv_R0 : forall x y:R, Un_cv (Majxy x y) 0.
intros.
-pose (C := Rmax 1 (Rmax (Rabs x) (Rabs y))).
-pose (C0 := C ^ 4).
+set (C := Rmax 1 (Rmax (Rabs x) (Rabs y))).
+set (C0 := C ^ 4).
cut (0 < C).
intro.
cut (0 < C0).
@@ -69,7 +69,7 @@ Lemma reste1_maj :
forall (x y:R) (N:nat),
(0 < N)%nat -> Rabs (Reste1 x y N) <= Majxy x y (pred N).
intros.
-pose (C := Rmax 1 (Rmax (Rabs x) (Rabs y))).
+set (C := Rmax 1 (Rmax (Rabs x) (Rabs y))).
unfold Reste1 in |- *.
apply Rle_trans with
(sum_f_R0
@@ -454,7 +454,7 @@ Qed.
Lemma reste2_maj :
forall (x y:R) (N:nat), (0 < N)%nat -> Rabs (Reste2 x y N) <= Majxy x y N.
intros.
-pose (C := Rmax 1 (Rmax (Rabs x) (Rabs y))).
+set (C := Rmax 1 (Rmax (Rabs x) (Rabs y))).
unfold Reste2 in |- *.
apply Rle_trans with
(sum_f_R0
@@ -926,8 +926,8 @@ Qed.
Lemma reste_cv_R0 : forall x y:R, Un_cv (Reste x y) 0.
intros.
unfold Reste in |- *.
-pose (An := fun n:nat => Reste2 x y n).
-pose (Bn := fun n:nat => Reste1 x y (S n)).
+set (An := fun n:nat => Reste2 x y n).
+set (Bn := fun n:nat => Reste1 x y (S n)).
cut
(Un_cv (fun n:nat => An n - Bn n) (0 - 0) ->
Un_cv (fun N:nat => Reste2 x y N - Reste1 x y (S N)) 0).
@@ -979,7 +979,7 @@ cut (0 < eps / 3);
elim (H4 (eps / 3) H7); intros N1 H8.
elim (H5 (eps / 3) H7); intros N2 H9.
elim (H6 (eps / 3) H7); intros N3 H10.
-pose (N := S (S (max (max N1 N2) N3))).
+set (N := S (S (max (max N1 N2) N3))).
exists N.
intros.
cut (n = S (pred n)).
diff --git a/theories/Reals/Cos_rel.v b/theories/Reals/Cos_rel.v
index 5e9d26001f..1054f73ecb 100644
--- a/theories/Reals/Cos_rel.v
+++ b/theories/Reals/Cos_rel.v
@@ -98,7 +98,7 @@ replace
sum_f_R0
(fun l:nat => C (2 * k) (2 * l) * x ^ (2 * l) * y ^ (2 * (k - l))) k)
(S n)).
-pose
+set
(sin_nnn :=
fun n:nat =>
match n with
@@ -135,7 +135,7 @@ unfold sin_nnn in |- *.
rewrite <- Rmult_plus_distr_l.
apply Rmult_eq_compat_l.
rewrite binomial.
-pose (Wn := fun i0:nat => C (2 * S i) i0 * x ^ i0 * y ^ (2 * S i - i0)).
+set (Wn := fun i0:nat => C (2 * S i) i0 * x ^ i0 * y ^ (2 * S i - i0)).
replace
(sum_f_R0
(fun l:nat => C (2 * S i) (2 * l) * x ^ (2 * l) * y ^ (2 * (S i - l)))
diff --git a/theories/Reals/Exp_prop.v b/theories/Reals/Exp_prop.v
index c424b9e140..ffc3005045 100644
--- a/theories/Reals/Exp_prop.v
+++ b/theories/Reals/Exp_prop.v
@@ -114,7 +114,7 @@ Qed.
Lemma Reste_E_maj :
forall (x y:R) (N:nat),
(0 < N)%nat -> Rabs (Reste_E x y N) <= maj_Reste_E x y N.
-intros; pose (M := Rmax 1 (Rmax (Rabs x) (Rabs y))).
+intros; set (M := Rmax 1 (Rmax (Rabs x) (Rabs y))).
apply Rle_trans with
(M ^ (2 * N) *
sum_f_R0
@@ -742,7 +742,7 @@ Qed.
(**********)
Lemma exp_pos_pos : forall x:R, 0 < x -> 0 < exp x.
-intros; pose (An := fun N:nat => / INR (fact N) * x ^ N).
+intros; set (An := fun N:nat => / INR (fact N) * x ^ N).
cut (Un_cv (fun n:nat => sum_f_R0 An n) (exp x)).
intro; apply Rlt_le_trans with (sum_f_R0 An 0).
unfold An in |- *; simpl in |- *; rewrite Rinv_1; rewrite Rmult_1_r;
@@ -784,7 +784,7 @@ Qed.
(* ((exp h)-1)/h -> 0 quand h->0 *)
Lemma derivable_pt_lim_exp_0 : derivable_pt_lim exp 0 1.
unfold derivable_pt_lim in |- *; intros.
-pose (fn := fun (N:nat) (x:R) => x ^ N / INR (fact (S N))).
+set (fn := fun (N:nat) (x:R) => x ^ N / INR (fact (S N))).
cut (CVN_R fn).
intro; cut (forall x:R, sigT (fun l:R => Un_cv (fun N:nat => SP fn N x) l)).
intro cv; cut (forall n:nat, continuity (fn n)).
diff --git a/theories/Reals/MVT.v b/theories/Reals/MVT.v
index d7531e49f5..a6c2d115c5 100644
--- a/theories/Reals/MVT.v
+++ b/theories/Reals/MVT.v
@@ -25,7 +25,7 @@ Theorem MVT :
(g b - g a) * derive_pt f c (pr1 c P) =
(f b - f a) * derive_pt g c (pr2 c P)).
intros; assert (H2 := Rlt_le _ _ H).
-pose (h := fun y:R => (g b - g a) * f y - (f b - f a) * g y).
+set (h := fun y:R => (g b - g a) * f y - (f b - f a) * g y).
cut (forall c:R, a < c < b -> derivable_pt h c).
intro; cut (forall c:R, a <= c <= b -> continuity_pt h c).
intro; assert (H4 := continuity_ab_maj h a b H2 H3).
@@ -33,7 +33,7 @@ assert (H5 := continuity_ab_min h a b H2 H3).
elim H4; intros Mx H6.
elim H5; intros mx H7.
cut (h a = h b).
-intro; pose (M := h Mx); pose (m := h mx).
+intro; set (M := h Mx); set (m := h mx).
cut
(forall (c:R) (P:a < c < b),
derive_pt h c (X c P) =
diff --git a/theories/Reals/NewtonInt.v b/theories/Reals/NewtonInt.v
index e2080827bf..2d55efe780 100644
--- a/theories/Reals/NewtonInt.v
+++ b/theories/Reals/NewtonInt.v
@@ -288,7 +288,7 @@ assert (H6 := H _ H5); elim H6; clear H6; intros;
unfold derivable_pt_lim in |- *; assert (H7 : derive_pt F0 x x0 = f x).
symmetry in |- *; assumption.
assert (H8 := derive_pt_eq_1 F0 x (f x) x0 H7); unfold derivable_pt_lim in H8;
- intros; elim (H8 _ H9); intros; pose (D := Rmin x1 (b - x)).
+ intros; elim (H8 _ H9); intros; set (D := Rmin x1 (b - x)).
assert (H11 : 0 < D).
unfold D in |- *; unfold Rmin in |- *; case (Rle_dec x1 (b - x)); intro.
apply (cond_pos x1).
@@ -335,7 +335,7 @@ assert (H11 := derive_pt_eq_1 F0 x (f x) x1 H9);
| right _ => F1 x + (F0 b - F1 b)
end) x (f x)).
unfold derivable_pt_lim in |- *; unfold derivable_pt_lim in H11, H12; intros;
- elim (H11 _ H13); elim (H12 _ H13); intros; pose (D := Rmin x2 x3);
+ elim (H11 _ H13); elim (H12 _ H13); intros; set (D := Rmin x2 x3);
assert (H16 : 0 < D).
unfold D in |- *; unfold Rmin in |- *; case (Rle_dec x2 x3); intro.
apply (cond_pos x2).
@@ -375,7 +375,7 @@ assert (H6 := H0 _ H5); elim H6; clear H6; intros;
unfold derivable_pt_lim in |- *; assert (H7 : derive_pt F1 x x0 = f x).
symmetry in |- *; assumption.
assert (H8 := derive_pt_eq_1 F1 x (f x) x0 H7); unfold derivable_pt_lim in H8;
- intros; elim (H8 _ H9); intros; pose (D := Rmin x1 (x - b));
+ intros; elim (H8 _ H9); intros; set (D := Rmin x1 (x - b));
assert (H11 : 0 < D).
unfold D in |- *; unfold Rmin in |- *; case (Rle_dec x1 (x - b)); intro.
apply (cond_pos x1).
@@ -462,7 +462,7 @@ Lemma NewtonInt_P7 :
Newton_integrable f b c -> Newton_integrable f a c.
unfold Newton_integrable in |- *; intros f a b c Hab Hbc X X0; elim X;
clear X; intros F0 H0; elim X0; clear X0; intros F1 H1;
- pose
+ set
(g :=
fun x:R =>
match Rle_dec x b with
diff --git a/theories/Reals/PSeries_reg.v b/theories/Reals/PSeries_reg.v
index b6375829bf..130f3b6596 100644
--- a/theories/Reals/PSeries_reg.v
+++ b/theories/Reals/PSeries_reg.v
@@ -110,7 +110,7 @@ elim H6; intros del1 H7.
unfold continuity_pt in H5; unfold continue_in in H5; unfold limit1_in in H5;
unfold limit_in in H5; simpl in H5; unfold R_dist in H5.
elim (H5 _ H3); intros del2 H8.
-pose (del := Rmin del1 del2).
+set (del := Rmin del1 del2).
exists del; intros.
split.
unfold del in |- *; unfold Rmin in |- *; case (Rle_dec del1 del2); intro.
@@ -226,7 +226,7 @@ Lemma CVN_R_CVS :
forall fn:nat -> R -> R,
CVN_R fn -> forall x:R, sigT (fun l:R => Un_cv (fun N:nat => SP fn N x) l).
intros; apply R_complete.
-unfold SP in |- *; pose (An := fun N:nat => fn N x).
+unfold SP in |- *; set (An := fun N:nat => fn N x).
change (Cauchy_crit_series An) in |- *.
apply cauchy_abs.
unfold Cauchy_crit_series in |- *; apply CV_Cauchy.
diff --git a/theories/Reals/PartSum.v b/theories/Reals/PartSum.v
index c12aea9df6..6a65ade8b3 100644
--- a/theories/Reals/PartSum.v
+++ b/theories/Reals/PartSum.v
@@ -212,7 +212,7 @@ assumption.
cut (0 < Rabs ((l1 - l2) / 2)); [ intro | apply Rabs_pos_lt ].
elim (H (Rabs ((l1 - l2) / 2)) H2); intros.
elim (H0 (Rabs ((l1 - l2) / 2)) H2); intros.
-pose (N := max x0 x); cut (N >= x0)%nat.
+set (N := max x0 x); cut (N >= x0)%nat.
cut (N >= x)%nat.
intros; assert (H7 := H3 N H5); assert (H8 := H4 N H6).
cut (Rabs (l1 - l2) <= R_dist (sum_f_R0 An N) l1 + R_dist (sum_f_R0 An N) l2).
@@ -390,7 +390,7 @@ do 2 rewrite Rabs_Ropp.
rewrite
(Rabs_right (sum_f_R0 (fun i:nat => Rabs (An (S n + i)%nat)) (m - S n)))
.
-pose (Bn := fun i:nat => An (S n + i)%nat).
+set (Bn := fun i:nat => An (S n + i)%nat).
replace (fun i:nat => Rabs (An (S n + i)%nat)) with
(fun i:nat => Rabs (Bn i)).
apply Rabs_triang_gen.
@@ -415,7 +415,7 @@ do 2 rewrite Rplus_0_r.
rewrite
(Rabs_right (sum_f_R0 (fun i:nat => Rabs (An (S m + i)%nat)) (n - S m)))
.
-pose (Bn := fun i:nat => An (S m + i)%nat).
+set (Bn := fun i:nat => An (S m + i)%nat).
replace (fun i:nat => Rabs (An (S m + i)%nat)) with
(fun i:nat => Rabs (Bn i)).
apply Rabs_triang_gen.
@@ -489,11 +489,11 @@ elim s; intro.
left; apply a.
right; apply b.
cut (Un_growing (fun n:nat => sum_f_R0 An n)).
-intro; pose (l1 := sum_f_R0 An N).
+intro; set (l1 := sum_f_R0 An N).
fold l1 in r.
unfold Un_cv in H; cut (0 < l1 - l).
intro; elim (H _ H2); intros.
-pose (N0 := max x N); cut (N0 >= x)%nat.
+set (N0 := max x N); cut (N0 >= x)%nat.
intro; assert (H5 := H3 N0 H4).
cut (l1 <= sum_f_R0 An N0).
intro; unfold R_dist in H5; rewrite Rabs_right in H5.
@@ -534,7 +534,7 @@ intro; cut (0 < (Rabs l1 - l2) / 2).
intro; unfold Un_cv in H, H0.
elim (H _ H3); intros Na H4.
elim (H0 _ H3); intros Nb H5.
-pose (N := max Na Nb).
+set (N := max Na Nb).
unfold R_dist in H4, H5.
cut (Rabs (sum_f_R0 An N - l2) < (Rabs l1 - l2) / 2).
intro; cut (Rabs (Rabs l1 - Rabs (SP fn N x)) < (Rabs l1 - l2) / 2).
diff --git a/theories/Reals/Ranalysis1.v b/theories/Reals/Ranalysis1.v
index b7d4902254..868ca35fc5 100644
--- a/theories/Reals/Ranalysis1.v
+++ b/theories/Reals/Ranalysis1.v
@@ -931,7 +931,7 @@ reflexivity.
replace (fun y:R => y ^ S n) with (fun y:R => y * y ^ n).
replace (pred (S n)) with n; [ idtac | reflexivity ].
replace (fun y:R => y * y ^ n) with (id * (fun y:R => y ^ n))%F.
-pose (f := fun y:R => y ^ n).
+set (f := fun y:R => y ^ n).
replace (INR (S n) * x ^ n) with (1 * f x + id x * (INR n * x ^ pred n)).
apply derivable_pt_lim_mult.
apply derivable_pt_lim_id.
diff --git a/theories/Reals/Rcomplete.v b/theories/Reals/Rcomplete.v
index 53624cbb2d..5887e8ef06 100644
--- a/theories/Reals/Rcomplete.v
+++ b/theories/Reals/Rcomplete.v
@@ -26,8 +26,8 @@ Open Local Scope R_scope.
Theorem R_complete :
forall Un:nat -> R, Cauchy_crit Un -> sigT (fun l:R => Un_cv Un l).
intros.
-pose (Vn := sequence_minorant Un (cauchy_min Un H)).
-pose (Wn := sequence_majorant Un (cauchy_maj Un H)).
+set (Vn := sequence_minorant Un (cauchy_min Un H)).
+set (Wn := sequence_majorant Un (cauchy_maj Un H)).
assert (H0 := maj_cv Un H).
fold Wn in H0.
assert (H1 := min_cv Un H).
@@ -118,7 +118,7 @@ elim (p0 (eps / 5) H3); intros N2 H5.
unfold Cauchy_crit in H.
unfold R_dist in H.
elim (H (eps / 5) H3); intros N3 H6.
-pose (N := max (max N1 N2) N3).
+set (N := max (max N1 N2) N3).
apply Rle_lt_trans with (Rabs (x - Wn N) + Rabs (Wn N - x0)).
replace (x - x0) with (x - Wn N + (Wn N - x0)); [ apply Rabs_triang | ring ].
apply Rle_lt_trans with
diff --git a/theories/Reals/RiemannInt.v b/theories/Reals/RiemannInt.v
index 8b087856c6..7ebeed34b8 100644
--- a/theories/Reals/RiemannInt.v
+++ b/theories/Reals/RiemannInt.v
@@ -144,8 +144,8 @@ Lemma RiemannInt_P3 :
intros; case (Rle_dec a b); intro.
apply RiemannInt_P2 with f un wn; assumption.
assert (H1 : b <= a); auto with real.
-pose (vn' := fun n:nat => mkStepFun (StepFun_P6 (pre (vn n))));
- pose (wn' := fun n:nat => mkStepFun (StepFun_P6 (pre (wn n))));
+set (vn' := fun n:nat => mkStepFun (StepFun_P6 (pre (vn n))));
+ set (wn' := fun n:nat => mkStepFun (StepFun_P6 (pre (wn n))));
assert
(H2 :
forall n:nat,
@@ -221,7 +221,7 @@ unfold Un_cv in |- *; unfold R_dist in |- *; intros f; intros;
unfold Rdiv in |- *; apply Rmult_lt_0_compat;
[ assumption | apply Rinv_0_lt_compat; prove_sup0 ].
elim (H _ H3); clear H; intros N0 H; elim (H0 _ H3); clear H0; intros N1 H0;
- elim (H1 _ H3); clear H1; intros N2 H1; pose (N := max (max N0 N1) N2);
+ elim (H1 _ H3); clear H1; intros N2 H1; set (N := max (max N0 N1) N2);
exists N; intros;
apply Rle_lt_trans with
(Rabs
@@ -426,7 +426,7 @@ Lemma maxN :
forall (a b:R) (del:posreal),
a < b ->
sigT (fun n:nat => a + INR n * del < b /\ b <= a + INR (S n) * del).
-intros; pose (I := fun n:nat => a + INR n * del < b);
+intros; set (I := fun n:nat => a + INR n * del < b);
assert (H0 : exists n : nat, I n).
exists 0%nat; unfold I in |- *; rewrite Rmult_0_l; rewrite Rplus_0_r;
assumption.
@@ -487,7 +487,7 @@ Lemma Heine_cor1 :
a <= x <= b ->
a <= y <= b -> Rabs (x - y) < delta -> Rabs (f x - f y) < eps)).
intro f; intros;
- pose
+ set
(E :=
fun l:R =>
0 < l <= b - a /\
@@ -512,7 +512,7 @@ assert (H3 := completeness E H1 H2); elim H3; intros; cut (0 < x <= b - a).
intro; elim H4; clear H4; intros; apply existT with (mkposreal _ H4); split.
apply H5.
unfold is_lub in p; elim p; intros; unfold is_upper_bound in H6;
- pose (D := Rabs (x0 - y)); elim (classic (exists y : R, D < y /\ E y));
+ set (D := Rabs (x0 - y)); elim (classic (exists y : R, D < y /\ E y));
intro.
elim H11; intros; elim H12; clear H12; intros; unfold E in H13; elim H13;
intros; apply H15; assumption.
@@ -743,7 +743,7 @@ apply le_lt_n_Sm; assumption.
apply Rge_minus; apply Rle_ge; assumption.
intros; clear H0 H1 H4 phi H5 H6 t H7; case (Req_dec t0 b); intro.
left; assumption.
-right; pose (I := fun j:nat => a + INR j * del <= t0);
+right; set (I := fun j:nat => a + INR j * del <= t0);
assert (H1 : exists n : nat, I n).
exists 0%nat; unfold I in |- *; rewrite Rmult_0_l; rewrite Rplus_0_r; elim H8;
intros; assumption.
@@ -1070,7 +1070,7 @@ unfold Rdiv in |- *; apply Rmult_lt_0_compat;
[ assumption | apply Rinv_0_lt_compat; prove_sup0 ].
elim (H _ H4); clear H; intros N0 H.
elim (H2 _ H4); clear H2; intros N1 H2.
-pose (N := max N0 N1); exists N; intros; unfold R_dist in |- *.
+set (N := max N0 N1); exists N; intros; unfold R_dist in |- *.
apply Rle_lt_trans with
(Rabs (RiemannInt_SF (phi2 n) - RiemannInt_SF (phi1 n)) +
Rabs (RiemannInt_SF (phi1 n) - l)).
@@ -1142,7 +1142,7 @@ unfold Rdiv in |- *; apply Rmult_lt_0_compat;
[ assumption | apply Rinv_0_lt_compat; prove_sup0 ].
elim (H _ H4); clear H; intros N0 H.
elim (H2 _ H4); clear H2; intros N1 H2.
-pose (N := max N0 N1); exists N; intros; unfold R_dist in |- *.
+set (N := max N0 N1); exists N; intros; unfold R_dist in |- *.
apply Rle_lt_trans with
(Rabs (RiemannInt_SF (phi2 n) - RiemannInt_SF (phi1 n)) +
Rabs (RiemannInt_SF (phi1 n) - l)).
@@ -1242,8 +1242,8 @@ pattern l at 2 in |- *; rewrite H0; rewrite Rmult_0_l; rewrite Rplus_0_r;
case (RiemannInt_exists pr1 RinvN RinvN_cv); intros;
eapply UL_sequence;
[ apply u0
- | pose (psi1 := fun n:nat => projT1 (phi_sequence_prop RinvN pr1 n));
- pose (psi2 := fun n:nat => projT1 (phi_sequence_prop RinvN pr3 n));
+ | set (psi1 := fun n:nat => projT1 (phi_sequence_prop RinvN pr1 n));
+ set (psi2 := fun n:nat => projT1 (phi_sequence_prop RinvN pr3 n));
apply RiemannInt_P11 with f RinvN (phi_sequence RinvN pr1) psi1 psi2;
[ apply RinvN_cv
| intro; apply (projT2 (phi_sequence_prop RinvN pr1 n))
@@ -1277,7 +1277,7 @@ unfold Rdiv in |- *; apply Rmult_lt_0_compat;
[ prove_sup0 | apply Rabs_pos_lt; assumption ] ].
elim (u _ H5); clear u; intros N2 H6; assert (H7 := RinvN_cv);
unfold Un_cv in H7; elim (H7 _ H5); clear H7 H5; intros N3 H5;
- unfold R_dist in H3, H4, H5, H6; pose (N := max (max N0 N1) (max N2 N3)).
+ unfold R_dist in H3, H4, H5, H6; set (N := max (max N0 N1) (max N2 N3)).
assert (H7 : forall n:nat, (n >= N1)%nat -> RinvN n < eps / 5).
intros; replace (pos (RinvN n)) with (Rabs (RinvN n - 0));
[ unfold RinvN in |- *; apply H4; assumption
@@ -1508,9 +1508,9 @@ Lemma RiemannInt_P15 :
intros; unfold RiemannInt in |- *; case (RiemannInt_exists pr RinvN RinvN_cv);
intros; eapply UL_sequence.
apply u.
-pose (phi1 := fun N:nat => phi_sequence RinvN pr N);
+set (phi1 := fun N:nat => phi_sequence RinvN pr N);
change (Un_cv (fun N:nat => RiemannInt_SF (phi1 N)) (c * (b - a))) in |- *;
- pose (f := fct_cte c);
+ set (f := fct_cte c);
assert
(H1 :
exists psi1 : nat -> StepFun a b,
@@ -1522,8 +1522,8 @@ pose (phi1 := fun N:nat => phi_sequence RinvN pr N);
split with (fun n:nat => projT1 (phi_sequence_prop RinvN pr n)); intro;
apply (projT2 (phi_sequence_prop RinvN pr n)).
elim H1; clear H1; intros psi1 H1;
- pose (phi2 := fun n:nat => mkStepFun (StepFun_P4 a b c));
- pose (psi2 := fun n:nat => mkStepFun (StepFun_P4 a b 0));
+ set (phi2 := fun n:nat => mkStepFun (StepFun_P4 a b c));
+ set (psi2 := fun n:nat => mkStepFun (StepFun_P4 a b 0));
apply RiemannInt_P11 with f RinvN phi2 psi2 psi1;
try assumption.
apply RinvN_cv.
@@ -1559,7 +1559,7 @@ clear n; assert (H3 : 0 < (l1 - l2) / 2).
unfold Rdiv in |- *; apply Rmult_lt_0_compat;
[ apply Rlt_Rminus; assumption | apply Rinv_0_lt_compat; prove_sup0 ].
elim (H1 _ H3); elim (H0 _ H3); clear H0 H1; unfold R_dist in |- *; intros;
- pose (N := max x x0); cut (Vn N < Un N).
+ set (N := max x x0); cut (Vn N < Un N).
intro; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ (H N) H4)).
apply Rlt_trans with ((l1 + l2) / 2).
apply Rplus_lt_reg_r with (- l2);
@@ -1593,8 +1593,8 @@ Lemma RiemannInt_P17 :
intro f; intros; unfold RiemannInt in |- *;
case (RiemannInt_exists pr1 RinvN RinvN_cv);
case (RiemannInt_exists pr2 RinvN RinvN_cv); intros;
- pose (phi1 := phi_sequence RinvN pr1);
- pose (phi2 := fun N:nat => mkStepFun (StepFun_P32 (phi1 N)));
+ set (phi1 := phi_sequence RinvN pr1);
+ set (phi2 := fun N:nat => mkStepFun (StepFun_P32 (phi1 N)));
apply Rle_cv_lim with
(fun N:nat => Rabs (RiemannInt_SF (phi1 N)))
(fun N:nat => RiemannInt_SF (phi2 N)).
@@ -1603,7 +1603,7 @@ fold phi1 in u0;
apply (continuity_seq Rabs (fun N:nat => RiemannInt_SF (phi1 N)) x0);
try assumption.
apply Rcontinuity_abs.
-pose (phi3 := phi_sequence RinvN pr2);
+set (phi3 := phi_sequence RinvN pr2);
assert
(H0 :
exists psi3 : nat -> StepFun a b,
@@ -1652,7 +1652,7 @@ intro f; intros; unfold RiemannInt in |- *;
case (RiemannInt_exists pr2 RinvN RinvN_cv); intros;
eapply UL_sequence.
apply u0.
-pose (phi1 := fun N:nat => phi_sequence RinvN pr1 N);
+set (phi1 := fun N:nat => phi_sequence RinvN pr1 N);
change (Un_cv (fun N:nat => RiemannInt_SF (phi1 N)) x) in |- *;
assert
(H1 :
@@ -1665,8 +1665,8 @@ pose (phi1 := fun N:nat => phi_sequence RinvN pr1 N);
split with (fun n:nat => projT1 (phi_sequence_prop RinvN pr1 n)); intro;
apply (projT2 (phi_sequence_prop RinvN pr1 n)).
elim H1; clear H1; intros psi1 H1;
- pose (phi2 := fun N:nat => phi_sequence RinvN pr2 N).
-pose
+ set (phi2 := fun N:nat => phi_sequence RinvN pr2 N).
+set
(phi2_aux :=
fun (N:nat) (x:R) =>
match Req_EM_T x a with
@@ -1678,7 +1678,7 @@ pose
end
end).
cut (forall N:nat, IsStepFun (phi2_aux N) a b).
-intro; pose (phi2_m := fun N:nat => mkStepFun (X N)).
+intro; set (phi2_m := fun N:nat => mkStepFun (X N)).
assert
(H2 :
exists psi2 : nat -> StepFun a b,
@@ -1850,7 +1850,7 @@ unfold Rdiv in |- *; apply Rmult_lt_0_compat;
[ apply (cond_pos eps) | apply Rinv_0_lt_compat; prove_sup0 ].
elim (X (mkposreal _ H)); clear X; intros phi1 [psi1 H1];
elim (X0 (mkposreal _ H)); clear X0; intros phi2 [psi2 H2].
-pose
+set
(phi3 :=
fun x:R =>
match Rle_dec a x with
@@ -1861,7 +1861,7 @@ pose
end
| right _ => 0
end).
-pose
+set
(psi3 :=
fun x:R =>
match Rle_dec a x with
@@ -2276,7 +2276,7 @@ elim (u1 _ H0); clear u1; intros N1 H1; elim (u0 _ H0); clear u0;
(RiemannInt_SF (phi_sequence RinvN pr1 n) +
RiemannInt_SF (phi_sequence RinvN pr2 n))) 0).
intro; elim (H3 _ H0); clear H3; intros N3 H3;
- pose (N0 := max (max N1 N2) N3); exists N0; intros;
+ set (N0 := max (max N1 N2) N3); exists N0; intros;
unfold R_dist in |- *;
apply Rle_lt_trans with
(Rabs
@@ -2372,9 +2372,9 @@ unfold R_dist in |- *; unfold Rminus in |- *; rewrite Ropp_0;
left; apply (cond_pos (RinvN n)).
exists N0; intros; elim (H1 n); elim (H2 n); elim (H3 n); clear H1 H2 H3;
intros; unfold R_dist in |- *; unfold Rminus in |- *;
- rewrite Ropp_0; rewrite Rplus_0_r; pose (phi1 := phi_sequence RinvN pr1 n);
- fold phi1 in H8; pose (phi2 := phi_sequence RinvN pr2 n);
- fold phi2 in H3; pose (phi3 := phi_sequence RinvN pr3 n);
+ rewrite Ropp_0; rewrite Rplus_0_r; set (phi1 := phi_sequence RinvN pr1 n);
+ fold phi1 in H8; set (phi2 := phi_sequence RinvN pr2 n);
+ fold phi2 in H3; set (phi3 := phi_sequence RinvN pr3 n);
fold phi2 in H1; assert (H10 : IsStepFun phi3 a b).
apply StepFun_P44 with c.
apply (pre phi3).
@@ -2577,7 +2577,7 @@ unfold derivable_pt_lim in |- *; intros; assert (Hyp : 0 < eps / 2).
unfold Rdiv in |- *; apply Rmult_lt_0_compat;
[ assumption | apply Rinv_0_lt_compat; prove_sup0 ].
elim (H1 _ Hyp); unfold dist, D_x, no_cond in |- *; simpl in |- *;
- unfold R_dist in |- *; intros; pose (del := Rmin x0 (Rmin (b - x) (x - a)));
+ unfold R_dist in |- *; intros; set (del := Rmin x0 (Rmin (b - x) (x - a)));
assert (H4 : 0 < del).
unfold del in |- *; unfold Rmin in |- *; case (Rle_dec (b - x) (x - a));
intro.
@@ -2786,7 +2786,7 @@ intro f; intros; elim h; intro.
elim H; clear H; intros; elim H; intro.
elim H1; intro.
apply RiemannInt_P27; split; assumption.
-pose
+set
(f_b := fun x:R => f b * (x - b) + RiemannInt (FTC_P1 h C0 h (Rle_refl b)));
rewrite H3.
assert (H4 : derivable_pt_lim f_b b (f b)).
@@ -2815,7 +2815,7 @@ assert (H8 : 0 < eps / 2).
unfold Rdiv in |- *; apply Rmult_lt_0_compat;
[ assumption | apply Rinv_0_lt_compat; prove_sup0 ].
elim (H7 _ H8); unfold D_x, no_cond, dist in |- *; simpl in |- *;
- unfold R_dist in |- *; intros; pose (del := Rmin x0 (Rmin x1 (b - a)));
+ unfold R_dist in |- *; intros; set (del := Rmin x0 (Rmin x1 (b - a)));
assert (H10 : 0 < del).
unfold del in |- *; unfold Rmin in |- *; case (Rle_dec x1 (b - a)); intros.
case (Rle_dec x0 x1); intro;
@@ -2960,7 +2960,7 @@ unfold f_b in |- *; unfold Rminus in |- *; rewrite Rplus_opp_r;
| elim n; left; assumption
| elim n; right; reflexivity ].
(*****)
-pose (f_a := fun x:R => f a * (x - a)); rewrite <- H2;
+set (f_a := fun x:R => f a * (x - a)); rewrite <- H2;
assert (H3 : derivable_pt_lim f_a a (f a)).
unfold f_a in |- *;
change (derivable_pt_lim (fct_cte (f a) * (id - fct_cte a)%F) a (f a))
@@ -2981,7 +2981,7 @@ unfold Rdiv in |- *; apply Rmult_lt_0_compat;
[ assumption | apply Rinv_0_lt_compat; prove_sup0 ].
elim (H6 _ H7); unfold D_x, no_cond, dist in |- *; simpl in |- *;
unfold R_dist in |- *; intros.
-pose (del := Rmin x0 (Rmin x1 (b - a))).
+set (del := Rmin x0 (Rmin x1 (b - a))).
assert (H9 : 0 < del).
unfold del in |- *; unfold Rmin in |- *.
case (Rle_dec x1 (b - a)); intros.
@@ -3116,7 +3116,7 @@ rewrite Rplus_comm; apply Rle_trans with del;
(*****)
assert (H1 : x = a).
rewrite <- H0 in H; elim H; intros; apply Rle_antisym; assumption.
-pose (f_a := fun x:R => f a * (x - a)).
+set (f_a := fun x:R => f a * (x - a)).
assert (H2 : derivable_pt_lim f_a a (f a)).
unfold f_a in |- *;
change (derivable_pt_lim (fct_cte (f a) * (id - fct_cte a)%F) a (f a))
@@ -3129,7 +3129,7 @@ apply derivable_pt_lim_minus.
apply derivable_pt_lim_id.
apply derivable_pt_lim_const.
unfold fct_cte in |- *; ring.
-pose
+set
(f_b := fun x:R => f b * (x - b) + RiemannInt (FTC_P1 h C0 h (Rle_refl b))).
assert (H3 : derivable_pt_lim f_b b (f b)).
unfold f_b in |- *; pattern (f b) at 2 in |- *; replace (f b) with (f b + 0).
@@ -3151,7 +3151,7 @@ unfold fct_cte in |- *; ring.
apply derivable_pt_lim_const.
ring.
unfold derivable_pt_lim in |- *; intros; elim (H2 _ H4); intros;
- elim (H3 _ H4); intros; pose (del := Rmin x0 x1).
+ elim (H3 _ H4); intros; set (del := Rmin x0 x1).
assert (H7 : 0 < del).
unfold del in |- *; unfold Rmin in |- *; case (Rle_dec x0 x1); intro.
apply (cond_pos x0).
diff --git a/theories/Reals/RiemannInt_SF.v b/theories/Reals/RiemannInt_SF.v
index 19782f2bcb..f0b4793ebf 100644
--- a/theories/Reals/RiemannInt_SF.v
+++ b/theories/Reals/RiemannInt_SF.v
@@ -31,7 +31,7 @@ Lemma Nzorn :
forall I:nat -> Prop,
(exists n : nat, I n) ->
Nbound I -> sigT (fun n:nat => I n /\ (forall i:nat, I i -> (i <= n)%nat)).
-intros I H H0; pose (E := fun x:R => exists i : nat, I i /\ INR i = x);
+intros I H H0; set (E := fun x:R => exists i : nat, I i /\ INR i = x);
assert (H1 : bound E).
unfold Nbound in H0; elim H0; intros N H1; unfold bound in |- *;
exists (INR N); unfold is_upper_bound in |- *; intros;
@@ -534,7 +534,7 @@ rewrite <- H4; apply RList_P7;
clear Hrecs3; induction lf2 as [| r5 lf2 Hreclf2].
simpl in H11; discriminate.
clear Hreclf2; assert (H17 : r3 = r4).
-pose (x := (r + s2) / 2); assert (H17 := H8 0%nat (lt_O_Sn _));
+set (x := (r + s2) / 2); assert (H17 := H8 0%nat (lt_O_Sn _));
assert (H18 := H13 0%nat (lt_O_Sn _));
unfold constant_D_eq, open_interval in H17, H18; simpl in H17;
simpl in H18; rewrite <- (H17 x).
@@ -578,7 +578,7 @@ assert (H19 : r3 = r5).
assert (H19 := H7 1%nat); simpl in H19;
assert (H20 := H19 (lt_n_S _ _ (lt_O_Sn _))); elim H20;
intro.
-pose (x := (s2 + Rmin r1 r0) / 2); assert (H22 := H8 0%nat);
+set (x := (s2 + Rmin r1 r0) / 2); assert (H22 := H8 0%nat);
assert (H23 := H13 1%nat); simpl in H22; simpl in H23;
rewrite <- (H22 (lt_O_Sn _) x).
rewrite <- (H23 (lt_n_S _ _ (lt_O_Sn _)) x).
@@ -703,7 +703,7 @@ case (Req_dec r r1); intro.
right; assumption.
left; cut (r1 <= s2).
intro; unfold adapted_couple in H2, H; decompose [and] H; decompose [and] H2;
- clear H H2; pose (x := (r + r1) / 2); assert (H18 := H14 0%nat);
+ clear H H2; set (x := (r + r1) / 2); assert (H18 := H14 0%nat);
assert (H20 := H19 0%nat); unfold constant_D_eq, open_interval in H18, H20;
simpl in H18; simpl in H20; rewrite <- (H18 (lt_O_Sn _) x).
rewrite <- (H20 (lt_O_Sn _) x).
@@ -1148,7 +1148,7 @@ apply lt_n_Sm_le; apply lt_n_S; assumption.
apply lt_pred_n_n; apply neq_O_lt; red in |- *; intro; rewrite <- H13 in H8;
elim (lt_n_O _ H8).
rewrite H0; assumption.
-pose
+set
(I :=
fun j:nat =>
pos_Rl lf j <= pos_Rl (cons_ORlist lf lg) i /\ (j < Rlength lf)%nat);
@@ -1395,7 +1395,7 @@ apply lt_n_Sm_le; apply lt_n_S; assumption.
apply lt_pred_n_n; apply neq_O_lt; red in |- *; intro; rewrite <- H13 in H8;
elim (lt_n_O _ H8).
rewrite H0; assumption.
-pose
+set
(I :=
fun j:nat =>
pos_Rl lg j <= pos_Rl (cons_ORlist lf lg) i /\ (j < Rlength lg)%nat);
@@ -1774,7 +1774,7 @@ reflexivity.
assert (H4 : pos_Rl (cons r1 l) (pred (Rlength (cons r1 l))) = b).
rewrite <- H1; reflexivity.
elim (IHl r1 H2 H3 H4); intros g [H5 H6].
-pose
+set
(g' :=
fun x:R => match Rle_dec r1 x with
| left _ => g x
diff --git a/theories/Reals/Rpower.v b/theories/Reals/Rpower.v
index 30f7be1f03..20382b0857 100644
--- a/theories/Reals/Rpower.v
+++ b/theories/Reals/Rpower.v
@@ -146,7 +146,7 @@ symmetry in |- *; apply derive_pt_eq_0; apply derivable_pt_lim_exp.
Qed.
Lemma ln_exists1 : forall y:R, 0 < y -> 1 <= y -> sigT (fun z:R => y = exp z).
-intros; pose (f := fun x:R => exp x - y); cut (f 0 <= 0).
+intros; set (f := fun x:R => exp x - y); cut (f 0 <= 0).
intro; cut (continuity f).
intro; cut (0 <= f y).
intro; cut (f 0 * f y <= 0).
@@ -560,7 +560,7 @@ Lemma derivable_pt_lim_ln : forall x:R, 0 < x -> derivable_pt_lim ln x (/ x).
intros; assert (H0 := Dln x H); unfold D_in in H0; unfold limit1_in in H0;
unfold limit_in in H0; simpl in H0; unfold R_dist in H0;
unfold derivable_pt_lim in |- *; intros; elim (H0 _ H1);
- intros; elim H2; clear H2; intros; pose (alp := Rmin x0 (x / 2));
+ intros; elim H2; clear H2; intros; set (alp := Rmin x0 (x / 2));
assert (H4 : 0 < alp).
unfold alp in |- *; unfold Rmin in |- *; case (Rle_dec x0 (x / 2)); intro.
apply H2.
diff --git a/theories/Reals/Rsqrt_def.v b/theories/Reals/Rsqrt_def.v
index b123f1bb75..932e407732 100644
--- a/theories/Reals/Rsqrt_def.v
+++ b/theories/Reals/Rsqrt_def.v
@@ -267,7 +267,7 @@ unfold cv_infty in |- *.
intro.
case (total_order_T 0 M); intro.
elim s; intro.
-pose (N := up M).
+set (N := up M).
cut (0 <= N)%Z.
intro.
elim (IZN N H0); intros N0 H1.
@@ -475,8 +475,8 @@ apply dicho_up_decreasing; assumption.
assumption.
right; reflexivity.
2: left; assumption.
-pose (Vn := fun n:nat => dicho_lb x y (fun z:R => cond_positivity (f z)) n).
-pose (Wn := fun n:nat => dicho_up x y (fun z:R => cond_positivity (f z)) n).
+set (Vn := fun n:nat => dicho_lb x y (fun z:R => cond_positivity (f z)) n).
+set (Wn := fun n:nat => dicho_up x y (fun z:R => cond_positivity (f z)) n).
cut ((forall n:nat, f (Vn n) <= 0) -> f x0 <= 0).
cut ((forall n:nat, 0 <= f (Wn n)) -> 0 <= f x0).
intros.
@@ -652,7 +652,7 @@ Qed.
Lemma Rsqrt_exists :
forall y:R, 0 <= y -> sigT (fun z:R => 0 <= z /\ y = Rsqr z).
intros.
-pose (f := fun x:R => Rsqr x - y).
+set (f := fun x:R => Rsqr x - y).
cut (f 0 <= 0).
intro.
cut (continuity f).
diff --git a/theories/Reals/Rtopology.v b/theories/Reals/Rtopology.v
index 75385b4248..4c9a94031d 100644
--- a/theories/Reals/Rtopology.v
+++ b/theories/Reals/Rtopology.v
@@ -64,7 +64,7 @@ Lemma interior_P3 : forall D:R -> Prop, open_set (interior D).
intro; unfold open_set, interior in |- *; unfold neighbourhood in |- *;
intros; elim H; intros.
exists x0; unfold included in |- *; intros.
-pose (del := x0 - Rabs (x - x1)).
+set (del := x0 - Rabs (x - x1)).
cut (0 < del).
intro; exists (mkposreal del H2); intros.
cut (included (disc x1 (mkposreal del H2)) (disc x x0)).
@@ -108,7 +108,7 @@ Lemma adherence_P3 : forall D:R -> Prop, closed_set (adherence D).
intro; unfold closed_set, adherence in |- *;
unfold open_set, complementary, point_adherent in |- *;
intros;
- pose
+ set
(P :=
fun V:R -> Prop =>
neighbourhood V x -> exists y : R, intersection_domain V D y);
@@ -121,7 +121,7 @@ assert (H8 := H7 V0);
cut (exists delta : posreal, (forall x:R, disc x1 delta x -> V0 x)).
intro; assert (H10 := H8 H9); elim H4; assumption.
cut (0 < x0 - Rabs (x - x1)).
-intro; pose (del := mkposreal _ H9); exists del; intros;
+intro; set (del := mkposreal _ H9); exists del; intros;
unfold included in H5; apply H5; unfold disc in |- *;
apply Rle_lt_trans with (Rabs (x2 - x1) + Rabs (x1 - x)).
replace (x2 - x) with (x2 - x1 + (x1 - x)); [ apply Rabs_triang | ring ].
@@ -198,7 +198,7 @@ assert (H4 := H _ H2); assert (H5 := H0 _ H3);
unfold intersection_domain in |- *; unfold neighbourhood in H4, H5;
elim H4; clear H; intros del1 H; elim H5; clear H0;
intros del2 H0; cut (0 < Rmin del1 del2).
-intro; pose (del := mkposreal _ H6).
+intro; set (del := mkposreal _ H6).
exists del; unfold included in |- *; intros; unfold included in H, H0;
unfold disc in H, H0, H7.
split.
@@ -228,7 +228,7 @@ elim H; intros; apply H1.
unfold eq_Dom in |- *; split.
unfold included, interior, disc in |- *; intros;
cut (0 < del - Rabs (x - x0)).
-intro; pose (del2 := mkposreal _ H3).
+intro; set (del2 := mkposreal _ H3).
exists del2; unfold included in |- *; intros.
apply Rle_lt_trans with (Rabs (x1 - x0) + Rabs (x0 - x)).
replace (x1 - x) with (x1 - x0 + (x0 - x)); [ apply Rabs_triang | ring ].
@@ -333,7 +333,7 @@ Theorem Rsepare :
(exists W : R -> Prop,
neighbourhood V x /\
neighbourhood W y /\ ~ (exists y : R, intersection_domain V W y)).
-intros x y Hsep; pose (D := Rabs (x - y)).
+intros x y Hsep; set (D := Rabs (x - y)).
cut (0 < D / 2).
intro; exists (disc x (mkposreal _ H)).
exists (disc y (mkposreal _ H)); split.
@@ -431,16 +431,16 @@ Qed.
(**********)
Lemma compact_P1 : forall X:R -> Prop, compact X -> bounded X.
-intros; unfold compact in H; pose (D := fun x:R => True);
- pose (g := fun x y:R => Rabs y < x);
+intros; unfold compact in H; set (D := fun x:R => True);
+ set (g := fun x y:R => Rabs y < x);
cut (forall x:R, (exists y : _, g x y) -> True);
[ intro | intro; trivial ].
-pose (f0 := mkfamily D g H0); assert (H1 := H f0);
+set (f0 := mkfamily D g H0); assert (H1 := H f0);
cut (covering_open_set X f0).
intro; assert (H3 := H1 H2); elim H3; intros D' H4;
unfold covering_finite in H4; elim H4; intros; unfold family_finite in H6;
unfold domain_finite in H6; elim H6; intros l H7;
- unfold bounded in |- *; pose (r := MaxRlist l).
+ unfold bounded in |- *; set (r := MaxRlist l).
exists (- r); exists r; intros.
unfold covering in H5; assert (H9 := H5 _ H8); elim H9; intros;
unfold subfamily in H10; simpl in H10; elim H10; intros;
@@ -496,17 +496,17 @@ unfold included in |- *; unfold adherence in |- *;
assert (H1 := classic (X x)); elim H1; clear H1; intro.
assumption.
cut (forall y:R, X y -> 0 < Rabs (y - x) / 2).
-intro; pose (D := X);
- pose (g := fun y z:R => Rabs (y - z) < Rabs (y - x) / 2 /\ D y);
+intro; set (D := X);
+ set (g := fun y z:R => Rabs (y - z) < Rabs (y - x) / 2 /\ D y);
cut (forall x:R, (exists y : _, g x y) -> D x).
-intro; pose (f0 := mkfamily D g H3); assert (H4 := H f0);
+intro; set (f0 := mkfamily D g H3); assert (H4 := H f0);
cut (covering_open_set X f0).
intro; assert (H6 := H4 H5); elim H6; clear H6; intros D' H6.
unfold covering_finite in H6; decompose [and] H6;
unfold covering, subfamily in H7; simpl in H7;
unfold family_finite, subfamily in H8; simpl in H8;
unfold domain_finite in H8; elim H8; clear H8; intros l H8;
- pose (alp := MinRlist (AbsList l x)); cut (0 < alp).
+ set (alp := MinRlist (AbsList l x)); cut (0 < alp).
intro; assert (H10 := H0 (disc x (mkposreal _ H9)));
cut (neighbourhood (disc x (mkposreal alp H9)) x).
intro; assert (H12 := H10 H11); elim H12; clear H12; intros y H12;
@@ -596,7 +596,7 @@ Qed.
Lemma compact_P3 : forall a b:R, compact (fun c:R => a <= c <= b).
intros; case (Rle_dec a b); intro.
unfold compact in |- *; intros;
- pose
+ set
(A :=
fun x:R =>
a <= x <= b /\
@@ -617,7 +617,7 @@ intro; elim H9; clear H9; intros x H9; elim H9; clear H9; intros;
case (Req_dec m b); intro.
rewrite H11 in H10; rewrite H11 in H8; unfold A in H9; elim H9; clear H9;
intros; elim H12; clear H12; intros Dx H12;
- pose (Db := fun x:R => Dx x \/ x = y0); exists Db;
+ set (Db := fun x:R => Dx x \/ x = y0); exists Db;
unfold covering_finite in |- *; split.
unfold covering in |- *; unfold covering_finite in H12; elim H12; clear H12;
intros; unfold covering in H12; case (Rle_dec x0 x);
@@ -663,7 +663,7 @@ intros _ H16; assert (H17 := H16 H15); simpl in H17;
unfold intersection_domain in H17; split.
elim H17; intros; assumption.
unfold Db in |- *; left; elim H17; intros; assumption.
-pose (m' := Rmin (m + eps / 2) b); cut (A m').
+set (m' := Rmin (m + eps / 2) b); cut (A m').
intro; elim H3; intros; unfold is_upper_bound in H13;
assert (H15 := H13 m' H12); cut (m < m').
intro; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H15 H16)).
@@ -689,7 +689,7 @@ assumption.
elim H11; assumption.
unfold m' in |- *; apply Rmin_r.
unfold A in H9; elim H9; clear H9; intros; elim H12; clear H12; intros Dx H12;
- pose (Db := fun x:R => Dx x \/ x = y0); exists Db;
+ set (Db := fun x:R => Dx x \/ x = y0); exists Db;
unfold covering_finite in |- *; split.
unfold covering in |- *; unfold covering_finite in H12; elim H12; clear H12;
intros; unfold covering in H12; case (Rle_dec x0 x);
@@ -759,7 +759,7 @@ intro; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H13 H14)).
pattern m at 2 in |- *; rewrite <- Rplus_0_r; unfold Rminus in |- *;
apply Rplus_lt_compat_l; apply Ropp_lt_cancel; rewrite Ropp_involutive;
rewrite Ropp_0; apply (cond_pos eps).
-pose (P := fun n:R => A n /\ m - eps < n <= m);
+set (P := fun n:R => A n /\ m - eps < n <= m);
assert (H12 := not_ex_all_not _ P H9); unfold P in H12;
unfold is_upper_bound in |- *; intros;
assert (H14 := not_and_or _ _ (H12 x)); elim H14;
@@ -785,7 +785,7 @@ unfold A in |- *; split.
split; [ right; reflexivity | apply r ].
unfold covering_open_set in H; elim H; clear H; intros; unfold covering in H;
cut (a <= a <= b).
-intro; elim (H _ H1); intros y0 H2; pose (D' := fun x:R => x = y0); exists D';
+intro; elim (H _ H1); intros y0 H2; set (D' := fun x:R => x = y0); exists D';
unfold covering_finite in |- *; split.
unfold covering in |- *; simpl in |- *; intros; cut (x = a).
intro; exists y0; split.
@@ -812,11 +812,11 @@ Lemma compact_P4 :
forall X F:R -> Prop, compact X -> closed_set F -> included F X -> compact F.
unfold compact in |- *; intros; elim (classic (exists z : R, F z));
intro Hyp_F_NE.
-pose (D := ind f0); pose (g := f f0); unfold closed_set in H0.
-pose (g' := fun x y:R => f0 x y \/ complementary F y /\ D x).
-pose (D' := D).
+set (D := ind f0); set (g := f f0); unfold closed_set in H0.
+set (g' := fun x y:R => f0 x y \/ complementary F y /\ D x).
+set (D' := D).
cut (forall x:R, (exists y : R, g' x y) -> D' x).
-intro; pose (f' := mkfamily D' g' H3); cut (covering_open_set X f').
+intro; set (f' := mkfamily D' g' H3); cut (covering_open_set X f').
intro; elim (H _ H4); intros DX H5; exists DX.
unfold covering_finite in |- *; unfold covering_finite in H5; elim H5;
clear H5; intros.
@@ -916,10 +916,10 @@ Lemma continuity_compact :
(forall x:R, continuity_pt f x) -> compact X -> compact (image_dir f X).
unfold compact in |- *; intros; unfold covering_open_set in H1.
elim H1; clear H1; intros.
-pose (D := ind f1).
-pose (g := fun x y:R => image_rec f0 (f1 x) y).
+set (D := ind f1).
+set (g := fun x y:R => image_rec f0 (f1 x) y).
cut (forall x:R, (exists y : R, g x y) -> D x).
-intro; pose (f' := mkfamily D g H3).
+intro; set (f' := mkfamily D g H3).
cut (covering_open_set X f').
intro; elim (H0 f' H4); intros D' H5; exists D'.
unfold covering_finite in H5; elim H5; clear H5; intros;
@@ -961,7 +961,7 @@ Lemma prolongement_C0 :
exists g : R -> R,
continuity g /\ (forall c:R, a <= c <= b -> g c = f c).
intros; elim H; intro.
-pose
+set
(h :=
fun x:R =>
match Rle_dec x a with
@@ -1363,11 +1363,11 @@ Lemma compact_P6 :
intersection_vide_in X g ->
exists D : R -> Prop, intersection_vide_finite_in X (subfamily g D).
intros X H Hyp g H0 H1.
-pose (D' := ind g).
-pose (f' := fun x y:R => complementary (g x) y /\ D' x).
+set (D' := ind g).
+set (f' := fun x y:R => complementary (g x) y /\ D' x).
assert (H2 : forall x:R, (exists y : R, f' x y) -> D' x).
intros; elim H2; intros; unfold f' in H3; elim H3; intros; assumption.
-pose (f0 := mkfamily D' f' H2).
+set (f0 := mkfamily D' f' H2).
unfold compact in H; assert (H3 : covering_open_set X f0).
unfold covering_open_set in |- *; split.
unfold covering in |- *; intros; unfold intersection_vide_in in H1;
@@ -1441,8 +1441,8 @@ intro; elim H1; intros; exists x; elim (ValAdh_un_prop un x); intros;
apply (H4 H2).
assert (H1 : exists z : R, X z).
exists (un 0%nat); apply H0.
-pose (D := fun x:R => exists n : nat, x = INR n).
-pose
+set (D := fun x:R => exists n : nat, x = INR n).
+set
(g :=
fun x:R =>
adherence (fun y:R => (exists p : nat, y = un p /\ x <= INR p) /\ D x)).
@@ -1454,7 +1454,7 @@ unfold neighbourhood in |- *; exists (mkposreal _ Rlt_0_1);
unfold included in |- *; trivial.
elim (H3 _ H4); intros; unfold intersection_domain in H5; decompose [and] H5;
assumption.
-pose (f0 := mkfamily D g H2).
+set (f0 := mkfamily D g H2).
assert (H3 := compact_P6 X H H1 f0).
elim (classic (exists l : R, ValAdh_un un l)); intro.
assumption.
@@ -1465,7 +1465,7 @@ elim H7; intros SF H8; unfold intersection_vide_finite_in in H8; elim H8;
clear H8; intros; unfold intersection_vide_in in H8;
elim (H8 0); intros _ H10; elim H10; unfold family_finite in H9;
unfold domain_finite in H9; elim H9; clear H9; intros l H9;
- pose (r := MaxRlist l); cut (D r).
+ set (r := MaxRlist l); cut (D r).
intro; unfold D in H11; elim H11; intros; exists (un x);
unfold intersection_family in |- *; simpl in |- *;
unfold intersection_domain in |- *; intros; split.
@@ -1583,7 +1583,7 @@ elim X_enc; clear X_enc; intros m X_enc; elim X_enc; clear X_enc;
assert (H1 : forall t:posreal, 0 < t / 2).
intro; unfold Rdiv in |- *; apply Rmult_lt_0_compat;
[ apply (cond_pos t) | apply Rinv_0_lt_compat; prove_sup0 ].
-pose
+set
(g :=
fun x y:R =>
X x /\
@@ -1597,7 +1597,7 @@ pose
assert (H2 : forall x:R, (exists y : R, g x y) -> X x).
intros; elim H2; intros; unfold g in H3; elim H3; clear H3; intros H3 _;
apply H3.
-pose (f' := mkfamily X g H2); unfold compact in H0;
+set (f' := mkfamily X g H2); unfold compact in H0;
assert (H3 : covering_open_set X f').
unfold covering_open_set in |- *; split.
unfold covering in |- *; intros; exists x; simpl in |- *; unfold g in |- *;
@@ -1607,7 +1607,7 @@ assert (H4 := H _ H3); unfold continuity_pt in H4; unfold continue_in in H4;
unfold limit1_in in H4; unfold limit_in in H4; simpl in H4;
unfold R_dist in H4; elim (H4 (eps / 2) (H1 eps));
intros;
- pose
+ set
(E :=
fun zeta:R =>
0 < zeta <= M - m /\
@@ -1675,7 +1675,7 @@ apply H4.
split.
elim H5; intros; apply H8.
apply H7.
-pose (d := x1 / 2 - Rabs (x0 - x)); assert (H7 : 0 < d).
+set (d := x1 / 2 - Rabs (x0 - x)); assert (H7 : 0 < d).
unfold d in |- *; apply Rlt_Rminus; elim H5; clear H5; intros;
unfold disc in H7; apply H7.
exists (mkposreal _ H7); unfold included in |- *; intros; split.
@@ -1716,7 +1716,7 @@ intros;
(forall z:R, Rabs (z - x) < del -> Rabs (f0 z - f0 x) < eps / 2) /\
included (g x) (fun z:R => Rabs (z - x) < del / 2)) H6);
elim H7; clear H7; intros l' H7; elim H7; clear H7;
- intros; pose (D := MinRlist l'); cut (0 < D / 2).
+ intros; set (D := MinRlist l'); cut (0 < D / 2).
intro; exists (mkposreal _ H9); intros; assert (H13 := H4 _ H10); elim H13;
clear H13; intros xi H13; assert (H14 : In xi l).
unfold g in H13; decompose [and] H13; elim (H5 xi); intros; apply H14; split;
@@ -1760,7 +1760,7 @@ unfold Rdiv in |- *; apply Rmult_lt_0_compat;
apply H15
| apply Rinv_0_lt_compat; prove_sup0 ].
intros; elim (H5 x); intros; elim (H8 H6); intros;
- pose
+ set
(E :=
fun zeta:R =>
0 < zeta <= M - m /\
diff --git a/theories/Reals/Rtrigo.v b/theories/Reals/Rtrigo.v
index 6cba456fb5..3ff1f07152 100644
--- a/theories/Reals/Rtrigo.v
+++ b/theories/Reals/Rtrigo.v
@@ -343,7 +343,7 @@ Definition cos_ub (a:R) : R := cos_approx a 4.
Lemma sin_lb_gt_0 : forall a:R, 0 < a -> a <= PI / 2 -> 0 < sin_lb a.
intros.
unfold sin_lb in |- *; unfold sin_approx in |- *; unfold sin_term in |- *.
-pose (Un := fun i:nat => a ^ (2 * i + 1) / INR (fact (2 * i + 1))).
+set (Un := fun i:nat => a ^ (2 * i + 1) / INR (fact (2 * i + 1))).
replace
(sum_f_R0
(fun i:nat => (-1) ^ i * (a ^ (2 * i + 1) / INR (fact (2 * i + 1)))) 3)
@@ -407,7 +407,7 @@ apply Rmult_lt_compat_l.
apply lt_INR_0; apply neq_O_lt.
assert (H2 := fact_neq_0 (2 * n + 1)).
red in |- *; intro; elim H2; symmetry in |- *; assumption.
-do 2 rewrite S_INR; rewrite plus_INR; rewrite mult_INR; pose (x := INR n);
+do 2 rewrite S_INR; rewrite plus_INR; rewrite mult_INR; set (x := INR n);
unfold INR in |- *.
replace ((2 * x + 1 + 1 + 1) * (2 * x + 1 + 1)) with (4 * x * x + 10 * x + 6);
[ idtac | ring ].
diff --git a/theories/Reals/Rtrigo_alt.v b/theories/Reals/Rtrigo_alt.v
index c1ffc68ea9..098d4c7301 100644
--- a/theories/Reals/Rtrigo_alt.v
+++ b/theories/Reals/Rtrigo_alt.v
@@ -61,7 +61,7 @@ cut
a + sum_f_R0 (fun i:nat => sin_term a (S i)) (pred (2 * n + 1)) <= sin a /\
sin a <= a + sum_f_R0 (fun i:nat => sin_term a (S i)) (pred (2 * (n + 1)))).
intro; apply H1.
-pose (Un := fun n:nat => a ^ (2 * S n + 1) / INR (fact (2 * S n + 1))).
+set (Un := fun n:nat => a ^ (2 * S n + 1) / INR (fact (2 * S n + 1))).
replace (pred (2 * n + 1)) with (2 * n)%nat.
replace (pred (2 * (n + 1))) with (S (2 * n)).
replace (sum_f_R0 (fun i:nat => sin_term a (S i)) (2 * n)) with
@@ -256,7 +256,7 @@ cut
cos a0 <=
1 + sum_f_R0 (fun i:nat => cos_term a0 (S i)) (pred (2 * (n0 + 1)))).
intro; apply H2.
-pose (Un := fun n:nat => a0 ^ (2 * S n) / INR (fact (2 * S n))).
+set (Un := fun n:nat => a0 ^ (2 * S n) / INR (fact (2 * S n))).
replace (pred (2 * n0 + 1)) with (2 * n0)%nat.
replace (pred (2 * (n0 + 1))) with (S (2 * n0)).
replace (sum_f_R0 (fun i:nat => cos_term a0 (S i)) (2 * n0)) with
diff --git a/theories/Reals/Rtrigo_reg.v b/theories/Reals/Rtrigo_reg.v
index ca0eb33dc6..dc20ff7dc7 100644
--- a/theories/Reals/Rtrigo_reg.v
+++ b/theories/Reals/Rtrigo_reg.v
@@ -121,7 +121,7 @@ Qed.
(**********)
Lemma continuity_cos : continuity cos.
-pose (fn := fun (N:nat) (x:R) => (-1) ^ N / INR (fact (2 * N)) * x ^ (2 * N)).
+set (fn := fun (N:nat) (x:R) => (-1) ^ N / INR (fact (2 * N)) * x ^ (2 * N)).
cut (CVN_R fn).
intro; cut (forall x:R, sigT (fun l:R => Un_cv (fun N:nat => SP fn N x) l)).
intro cv; cut (forall n:nat, continuity (fn n)).
@@ -299,12 +299,12 @@ Qed.
(* (sin h)/h -> 1 when h -> 0 *)
Lemma derivable_pt_lim_sin_0 : derivable_pt_lim sin 0 1.
unfold derivable_pt_lim in |- *; intros.
-pose
+set
(fn := fun (N:nat) (x:R) => (-1) ^ N / INR (fact (2 * N + 1)) * x ^ (2 * N)).
cut (CVN_R fn).
intro; cut (forall x:R, sigT (fun l:R => Un_cv (fun N:nat => SP fn N x) l)).
intro cv.
-pose (r := mkposreal _ Rlt_0_1).
+set (r := mkposreal _ Rlt_0_1).
cut (CVN_r fn r).
intro; cut (forall (n:nat) (y:R), Boule 0 r y -> continuity_pt (fn n) y).
intro; cut (Boule 0 r 0).
@@ -393,7 +393,7 @@ intro; unfold continuity_pt in H3; unfold continue_in in H3;
cut (0 < eps / 2); [ intro | assumption ].
elim (H3 _ H4); intros del_c H5.
cut (0 < Rmin del del_c).
-intro; pose (delta := mkposreal _ H6).
+intro; set (delta := mkposreal _ H6).
exists delta; intros.
rewrite Rplus_0_l; replace (cos h - cos 0) with (-2 * Rsqr (sin (h / 2))).
unfold Rminus in |- *; rewrite Ropp_0; rewrite Rplus_0_r.
@@ -498,7 +498,7 @@ cut (0 < eps / 2);
[ apply H1 | apply Rinv_0_lt_compat; prove_sup0 ] ].
elim (H0 _ H2); intros alp1 H3.
elim (H _ H2); intros alp2 H4.
-pose (alp := Rmin alp1 alp2).
+set (alp := Rmin alp1 alp2).
cut (0 < alp).
intro; exists (mkposreal _ H5); intros.
replace ((sin (x + h) - sin x) / h - cos x) with
diff --git a/theories/Reals/SeqProp.v b/theories/Reals/SeqProp.v
index 4f69514299..3f976cee90 100644
--- a/theories/Reals/SeqProp.v
+++ b/theories/Reals/SeqProp.v
@@ -493,7 +493,7 @@ Lemma approx_maj :
forall (Un:nat -> R) (pr:has_ub Un) (eps:R),
0 < eps -> exists k : nat, Rabs (majorant Un pr - Un k) < eps.
intros.
-pose (P := fun k:nat => Rabs (majorant Un pr - Un k) < eps).
+set (P := fun k:nat => Rabs (majorant Un pr - Un k) < eps).
unfold P in |- *.
cut
((exists k : nat, P k) ->
@@ -561,7 +561,7 @@ Lemma approx_min :
forall (Un:nat -> R) (pr:has_lb Un) (eps:R),
0 < eps -> exists k : nat, Rabs (minorant Un pr - Un k) < eps.
intros.
-pose (P := fun k:nat => Rabs (minorant Un pr - Un k) < eps).
+set (P := fun k:nat => Rabs (minorant Un pr - Un k) < eps).
unfold P in |- *.
cut
((exists k : nat, P k) ->
@@ -639,7 +639,7 @@ intros; cut (0 < eps / 2);
[ assumption | apply Rinv_0_lt_compat; prove_sup0 ] ].
elim (H (eps / 2) H2); intros.
elim (H0 (eps / 2) H2); intros.
-pose (N := max x x0).
+set (N := max x x0).
apply Rle_lt_trans with (Rabs (l1 - Un N) + Rabs (Un N - l2)).
replace (l1 - l2) with (l1 - Un N + (Un N - l2));
[ apply Rabs_triang | ring ].
@@ -660,7 +660,7 @@ cut (0 < eps / 2);
[ assumption | apply Rinv_0_lt_compat; prove_sup0 ] ].
elim (H (eps / 2) H2); intros.
elim (H0 (eps / 2) H2); intros.
-pose (N := max x x0).
+set (N := max x x0).
exists N; intros.
replace (An n + Bn n - (l1 + l2)) with (An n - l1 + (Bn n - l2));
[ idtac | ring ].
@@ -799,7 +799,7 @@ unfold Un_cv in H; unfold R_dist in H; unfold Un_cv in H0;
unfold R_dist in H0.
elim (H (eps / (2 * Rabs l2)) H8); intros N1 H9.
elim (H0 (eps / (2 * M)) H6); intros N2 H10.
-pose (N := max N1 N2).
+set (N := max N1 N2).
exists N; intros.
apply Rle_lt_trans with
(Rabs (An n * Bn n - An n * l2) + Rabs (An n * l2 - l1 * l2)).
@@ -997,7 +997,7 @@ right; assumption.
cut (0 < Un n - l).
intro; unfold Un_cv in H0; unfold R_dist in H0.
elim (H0 (Un n - l) H1); intros N1 H2.
-pose (N := max n N1).
+set (N := max n N1).
cut (Un n - l <= Un N - l).
intro; cut (Un N - l < Un n - l).
intro; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H3 H4)).
@@ -1111,9 +1111,9 @@ rewrite H1; unfold Rminus in |- *; rewrite Ropp_0; rewrite Rplus_0_r;
rewrite Rabs_R0; rewrite pow_ne_zero;
[ unfold Rdiv in |- *; rewrite Rmult_0_l; rewrite Rabs_R0; assumption
| red in |- *; intro; rewrite H3 in H2; elim (le_Sn_n _ H2) ].
-assert (H2 := Rabs_pos_lt x H1); pose (M := up (Rabs x)); cut (0 <= M)%Z.
+assert (H2 := Rabs_pos_lt x H1); set (M := up (Rabs x)); cut (0 <= M)%Z.
intro; elim (IZN M H3); intros M_nat H4.
-pose (Un := fun n:nat => Rabs x ^ (M_nat + n) / INR (fact (M_nat + n))).
+set (Un := fun n:nat => Rabs x ^ (M_nat + n) / INR (fact (M_nat + n))).
cut (Un_cv Un 0); unfold Un_cv in |- *; unfold R_dist in |- *; intros.
elim (H5 eps H0); intros N H6.
exists (M_nat + N)%nat; intros;
@@ -1130,7 +1130,7 @@ apply le_plus_l.
assumption.
apply le_plus_minus; apply le_trans with (M_nat + N)%nat;
[ apply le_plus_l | assumption ].
-pose (Vn := fun n:nat => Rabs x * (Un 0%nat / INR (S n))).
+set (Vn := fun n:nat => Rabs x * (Un 0%nat / INR (S n))).
cut (1 <= M_nat)%nat.
intro; cut (forall n:nat, 0 < Un n).
intro; cut (Un_decreasing Un).
@@ -1195,7 +1195,7 @@ elim s; intro.
exists 0%nat; intros.
apply Rlt_trans with 0; [ assumption | apply lt_INR_0; apply lt_O_Sn ].
exists 0%nat; intros; rewrite b; apply lt_INR_0; apply lt_O_Sn.
-pose (M0_z := up M0).
+set (M0_z := up M0).
assert (H10 := archimed M0).
cut (0 <= M0_z)%Z.
intro; elim (IZN _ H11); intros M0_nat H12.
diff --git a/theories/Reals/SeqSeries.v b/theories/Reals/SeqSeries.v
index 2c035cf837..602cd871b4 100644
--- a/theories/Reals/SeqSeries.v
+++ b/theories/Reals/SeqSeries.v
@@ -281,7 +281,7 @@ assert (H5 := cv_infty_cv_R0 _ H4 H1); assert (H6 : 0 < eps / 2)...
unfold Rdiv in |- *; apply Rmult_lt_0_compat...
apply Rinv_0_lt_compat; prove_sup...
elim (H _ H6); clear H; intros N1 H;
- pose (C := Rabs (sum_f_R0 (fun k:nat => An k * (Bn k - l)) N1));
+ set (C := Rabs (sum_f_R0 (fun k:nat => An k * (Bn k - l)) N1));
assert
(H7 :
exists N : nat,
@@ -309,7 +309,7 @@ ring...
discrR...
apply Rabs_no_R0...
apply Rabs_no_R0...
-elim H7; clear H7; intros N2 H7; pose (N := max N1 N2); exists (S N); intros;
+elim H7; clear H7; intros N2 H7; set (N := max N1 N2); exists (S N); intros;
unfold R_dist in |- *;
replace (sum_f_R0 (fun k:nat => An k * Bn k) n / sum_f_R0 An n - l) with
(sum_f_R0 (fun k:nat => An k * (Bn k - l)) n / sum_f_R0 An n)...
@@ -375,7 +375,7 @@ Lemma Cesaro_1 :
forall (An:nat -> R) (l:R),
Un_cv An l -> Un_cv (fun n:nat => sum_f_R0 An (pred n) / INR n) l.
Proof with trivial.
-intros Bn l H; pose (An := fun _:nat => 1)...
+intros Bn l H; set (An := fun _:nat => 1)...
assert (H0 : forall n:nat, 0 < An n)...
intro; unfold An in |- *; apply Rlt_0_1...
assert (H1 : forall n:nat, 0 < sum_f_R0 An n)...
@@ -385,7 +385,7 @@ unfold cv_infty in |- *; intro; case (Rle_dec M 0); intro...
exists 0%nat; intros; apply Rle_lt_trans with 0...
assert (H2 : 0 < M)...
auto with real...
-clear n; pose (m := up M); elim (archimed M); intros;
+clear n; set (m := up M); elim (archimed M); intros;
assert (H5 : (0 <= m)%Z)...
apply le_IZR; unfold m in |- *; simpl in |- *; left; apply Rlt_trans with M...
elim (IZN _ H5); intros; exists x; intros; unfold An in |- *; rewrite sum_cte;
diff --git a/theories/Reals/Sqrt_reg.v b/theories/Reals/Sqrt_reg.v
index def3cd0a4b..a4ec84154c 100644
--- a/theories/Reals/Sqrt_reg.v
+++ b/theories/Reals/Sqrt_reg.v
@@ -104,7 +104,7 @@ unfold continuity_pt in |- *; unfold continue_in in |- *;
unfold limit1_in in |- *; unfold limit_in in |- *;
unfold dist in |- *; simpl in |- *; unfold R_dist in |- *;
intros.
-pose (alpha := Rmin eps 1).
+set (alpha := Rmin eps 1).
exists alpha; intros.
split.
unfold alpha in |- *; unfold Rmin in |- *; case (Rle_dec eps 1); intro.
@@ -131,7 +131,7 @@ unfold continuity_pt in |- *; unfold continue_in in |- *;
cut (0 < eps / sqrt x).
intro; elim (H0 _ H2); intros alp_1 H3.
elim H3; intros.
-pose (alpha := alp_1 * x).
+set (alpha := alp_1 * x).
exists (Rmin alpha x); intros.
split.
change (0 < Rmin alpha x) in |- *; unfold Rmin in |- *;
@@ -228,7 +228,7 @@ Qed.
(* sqrt is derivable for all x>0 *)
Lemma derivable_pt_lim_sqrt :
forall x:R, 0 < x -> derivable_pt_lim sqrt x (/ (2 * sqrt x)).
-intros; pose (g := fun h:R => sqrt x + sqrt (x + h)).
+intros; set (g := fun h:R => sqrt x + sqrt (x + h)).
cut (continuity_pt g 0).
intro; cut (g 0 <> 0).
intro; assert (H2 := continuity_pt_inv g 0 H0 H1).
@@ -237,7 +237,7 @@ unfold derivable_pt_lim in |- *; intros; unfold continuity_pt in H2;
unfold limit_in in H2; simpl in H2; unfold R_dist in H2.
elim (H2 eps H3); intros alpha H4.
elim H4; intros.
-pose (alpha1 := Rmin alpha x).
+set (alpha1 := Rmin alpha x).
cut (0 < alpha1).
intro; exists (mkposreal alpha1 H7); intros.
replace ((sqrt (x + h) - sqrt x) / h) with (/ (sqrt x + sqrt (x + h))).
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-17 12:09:13 +0000