aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Reals/Rtrigo_reg.v
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2014-06-01 10:26:26 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2014-06-01 11:33:55 +0200
commit76adb57c72fccb4f3e416bd7f3927f4fff72178b (patch)
treef8d72073a2ea62d3e5c274c201ef06532ac57b61 /theories/Reals/Rtrigo_reg.v
parentbe01deca2b8ff22505adaa66f55f005673bf2d85 (diff)
Making those proofs which depend on names generated for the arguments
in Prop of constructors of inductive types independent of these names. Incidentally upgraded/simplified a couple of proofs, mainly in Reals. This prepares to the next commit about using names based on H for such hypotheses in Prop.
Diffstat (limited to 'theories/Reals/Rtrigo_reg.v')
-rw-r--r--theories/Reals/Rtrigo_reg.v14
1 files changed, 7 insertions, 7 deletions
diff --git a/theories/Reals/Rtrigo_reg.v b/theories/Reals/Rtrigo_reg.v
index fff4fec98..aafa3357e 100644
--- a/theories/Reals/Rtrigo_reg.v
+++ b/theories/Reals/Rtrigo_reg.v
@@ -176,14 +176,14 @@ Proof.
intro; rewrite H9 in H8; rewrite H10 in H8.
apply H8.
unfold SFL, sin.
- case (cv h); intros.
- case (exist_sin (Rsqr h)); intros.
+ case (cv h) as (x,HUn).
+ case (exist_sin (Rsqr h)) as (x0,Hsin).
unfold Rdiv; rewrite (Rinv_r_simpl_m h x0 H6).
eapply UL_sequence.
- apply u.
- unfold sin_in in s; unfold sin_n, infinite_sum in s;
+ apply HUn.
+ unfold sin_in in Hsin; unfold sin_n, infinite_sum in Hsin;
unfold SP, fn, Un_cv; intros.
- elim (s _ H10); intros N0 H11.
+ elim (Hsin _ H10); intros N0 H11.
exists N0; intros.
unfold R_dist; unfold R_dist in H11.
replace
@@ -194,9 +194,9 @@ Proof.
apply sum_eq; intros; apply Rmult_eq_compat_l; unfold Rsqr;
rewrite pow_sqr; reflexivity.
unfold SFL, sin.
- case (cv 0); intros.
+ case (cv 0) as (?,HUn).
eapply UL_sequence.
- apply u.
+ apply HUn.
unfold SP, fn; unfold Un_cv; intros; exists 1%nat; intros.
unfold R_dist;
replace