diff options
| author |  Yves Bertot <bertot@inria.fr> | 2014-09-23 13:11:24 +0200 |
|---|---|---|
| committer | Yves Bertot <bertot@inria.fr> | 2014-09-23 13:11:24 +0200 |
| commit | 13ab2df9ed3a5ea6b7455ea8a7da4341e7f2bcd5 (patch) | |
| tree | fd42f041d099700403dfc0a3af69ea5791ec5930 /theories/Reals/Rsqrt_def.v | |
| parent | 85355cfda7a01fa532f111ee7c4d522a8be8a399 (diff) | |
adds general facts in the Reals library, whose need was detected in
experiments about computing PI
Diffstat (limited to 'theories/Reals/Rsqrt_def.v')
| -rw-r--r-- | theories/Reals/Rsqrt_def.v | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/theories/Reals/Rsqrt_def.v b/theories/Reals/Rsqrt_def.v index 2e3d7f167..af6f2b3ec 100644 --- a/theories/Reals/Rsqrt_def.v +++ b/theories/Reals/Rsqrt_def.v @@ -450,6 +450,14 @@ Proof. assumption. Qed. +(* A general purpose corollary. *) +Lemma cv_pow_half : forall a, Un_cv (fun n => a/2^n) 0. +intros a; unfold Rdiv; replace 0 with (a * 0) by ring. +apply CV_mult. + intros eps ep; exists 0%nat; rewrite R_dist_eq; intros n _; assumption. +exact (cv_infty_cv_R0 pow_2_n pow_2_n_neq_R0 pow_2_n_infty). +Qed. + (** Intermediate Value Theorem *) Lemma IVT : forall (f:R -> R) (x y:R), |