diff options
Diffstat (limited to 'theories/Reals/RiemannInt_SF.v')
| -rw-r--r-- | theories/Reals/RiemannInt_SF.v | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/theories/Reals/RiemannInt_SF.v b/theories/Reals/RiemannInt_SF.v index ef5d37bff..f98b1a143 100644 --- a/theories/Reals/RiemannInt_SF.v +++ b/theories/Reals/RiemannInt_SF.v @@ -943,9 +943,8 @@ Lemma StepFun_P21 : forall (a b:R) (f:R -> R) (l:Rlist), is_subdivision f a b l -> adapted_couple f a b l (FF l f). Proof. - intros; unfold adapted_couple; unfold is_subdivision in X; - unfold adapted_couple in X; elim X; clear X; intros; - decompose [and] p; clear p; repeat split; try assumption. + intros * (x & H & H1 & H0 & H2 & H4). + repeat split; try assumption. apply StepFun_P20; rewrite H2; apply lt_O_Sn. intros; assert (H5 := H4 _ H3); unfold constant_D_eq, open_interval in H5; unfold constant_D_eq, open_interval; intros; |