aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Reals/RiemannInt_SF.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Reals/RiemannInt_SF.v')
-rw-r--r--theories/Reals/RiemannInt_SF.v5
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;