diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-10-16 14:32:13 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-10-16 14:32:13 +0000 |
| commit | d7604922b69e2b3b0423dcec15dbdb9ae6993fdf (patch) | |
| tree | b25ace6fc0855ae22c06c014d0fec636836b32c3 /theories/Reals/RiemannInt.v | |
| parent | e2461a701cbda7580763f478988d9946b5dddb9a (diff) | |
FTC_P2 maintenant dans RIneq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4646 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Reals/RiemannInt.v')
| -rw-r--r-- | theories/Reals/RiemannInt.v | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/theories/Reals/RiemannInt.v b/theories/Reals/RiemannInt.v index a1f7101ef..a44f3c1b5 100644 --- a/theories/Reals/RiemannInt.v +++ b/theories/Reals/RiemannInt.v @@ -817,10 +817,7 @@ Qed. Lemma FTC_P1 : (f:R->R;a,b:R) ``a<=b`` -> ((x:R)``a<=x<=b``->(continuity_pt f x)) -> ((x:R)``a<=x``->``x<=b``->(Riemann_integrable f a x)). Intros; Apply continuity_implies_RiemannInt; [Assumption | Intros; Apply H0; Elim H3; Intros; Split; Assumption Orelse Apply Rle_trans with x; Assumption]. Qed. - -Lemma FTC_P2 : (x:R) ``x<=x``. -Intro; Right; Reflexivity. -Qed. +V7only [Notation FTC_P2 := Rle_refl.]. Definition primitive [f:R->R;a,b:R;h:``a<=b``;pr:((x:R)``a<=x``->``x<=b``->(Riemann_integrable f a x))] : R->R := [x:R] Cases (total_order_Rle a x) of | (leftT r) => Cases (total_order_Rle x b) of |