diff options
| author |  barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-12-24 10:27:08 +0000 |
|---|---|---|
| committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-12-24 10:27:08 +0000 |
| commit | 38734c5e122e9a38cf5b8afc586f47abced11361 (patch) | |
| tree | 2227afa958bf809d9152b526e29f183b552e5e61 /theories/Reals/Rtrigo.v | |
| parent | c69ae2a1f05db124c19b7f326ca23e980f643198 (diff) | |
changement de pose en set (pose n'etait pas utilise avec la semantique
documentee).
Reste a retablir la semantique de pose.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5141 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Reals/Rtrigo.v')
| -rw-r--r-- | theories/Reals/Rtrigo.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Reals/Rtrigo.v b/theories/Reals/Rtrigo.v index 6cba456fb..3ff1f0715 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 ]. |