diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-01-19 22:21:34 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-01-19 22:21:34 +0000 |
| commit | db4e1d74309296a32b1ac3b331f9f00bca021166 (patch) | |
| tree | e801332c421c92b82b4264e1704f6ddacdf01b42 /theories/Reals/RiemannInt_SF.v | |
| parent | 3236048ce870a80d6278a59205917379d31e31bb (diff) | |
Clear sur hypothese non definie
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3534 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Reals/RiemannInt_SF.v')
| -rw-r--r-- | theories/Reals/RiemannInt_SF.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Reals/RiemannInt_SF.v b/theories/Reals/RiemannInt_SF.v index fd75ae4d8..a6c1c7a08 100644 --- a/theories/Reals/RiemannInt_SF.v +++ b/theories/Reals/RiemannInt_SF.v @@ -920,7 +920,7 @@ Pose g' := [x:R]Cases (total_order_Rle r1 x) of Assert H7 : ``r1<=b``. Rewrite <- H4; Apply RList_P7; [Assumption | Left; Reflexivity]. Assert H8 : (IsStepFun g' a b). -Unfold IsStepFun; Assert H8 := (pre g); Unfold IsStepFun in H8; Elim H8; Intros lg H9; Unfold is_subdivision in H9; Elim H9; Clear H9 H10; Intros lg2 H9; Split with (cons a lg); Unfold is_subdivision; Split with (cons (f a) lg2); Unfold adapted_couple in H9; Decompose [and] H9; Clear H9; Unfold adapted_couple; Repeat Split. +Unfold IsStepFun; Assert H8 := (pre g); Unfold IsStepFun in H8; Elim H8; Intros lg H9; Unfold is_subdivision in H9; Elim H9; Clear H9; Intros lg2 H9; Split with (cons a lg); Unfold is_subdivision; Split with (cons (f a) lg2); Unfold adapted_couple in H9; Decompose [and] H9; Clear H9; Unfold adapted_couple; Repeat Split. Unfold ordered_Rlist; Intros; Simpl in H9; Induction i. Simpl; Rewrite H12; Replace (Rmin r1 b) with r1. Simpl in H0; Rewrite <- H0; Apply (H O); Simpl; Apply lt_O_Sn. |