More proofs independent of the names generated by induction/elim over

a dependent elimination principle for Prop arguments.

2 files changed, 26 insertions, 26 deletions

diff --git a/theories/Reals/MVT.v b/theories/Reals/MVT.v
index 4b8d9af48..e3c5298d7 100644
--- a/theories/Reals/MVT.v
+++ b/theories/Reals/MVT.v
@@ -151,14 +151,14 @@ Proof.
   cut (forall c:R, a <= c <= b -> continuity_pt id c);
     [ intro | intros; apply derivable_continuous_pt; apply derivable_id ].
   assert (H2 := MVT f id a b X X0 H H0 H1).
-  elim H2; intros c H3; elim H3; intros.
+  destruct H2 as (c & P & H4).
   exists c; split.
-  cut (derive_pt id c (X0 c x) = derive_pt id c (derivable_pt_id c));
-    [ intro | apply pr_nu ].
+  cut (derive_pt id c (X0 c P) = derive_pt id c (derivable_pt_id c));
+    [ intro H5 | apply pr_nu ].
   rewrite H5 in H4; rewrite (derive_pt_id c) in H4; rewrite Rmult_1_r in H4;
-    rewrite <- H4; replace (derive_pt f c (X c x)) with (derive_pt f c (pr c));
+    rewrite <- H4; replace (derive_pt f c (X c P)) with (derive_pt f c (pr c));
       [ idtac | apply pr_nu ]; apply Rmult_comm.
-  apply x.
+  apply P.
 Qed.
 
 Theorem MVT_cor2 :
@@ -173,14 +173,14 @@ Proof.
   intro; cut (forall c:R, a <= c <= b -> derivable_pt id c).
   intro X1; cut (forall c:R, a < c < b -> derivable_pt id c).
   intro X2; cut (forall c:R, a <= c <= b -> continuity_pt id c).
-  intro; elim (MVT f id a b X0 X2 H H1 H2); intros; elim H3; clear H3; intros;
-    exists x; split.
-  cut (derive_pt id x (X2 x x0) = 1).
-  cut (derive_pt f x (X0 x x0) = f' x).
+  intro; elim (MVT f id a b X0 X2 H H1 H2); intros x (P,H3).
+  exists x; split.
+  cut (derive_pt id x (X2 x P) = 1).
+  cut (derive_pt f x (X0 x P) = f' x).
   intros; rewrite H4 in H3; rewrite H5 in H3; unfold id in H3;
     rewrite Rmult_1_r in H3; rewrite Rmult_comm; symmetry ;
       assumption.
-  apply derive_pt_eq_0; apply H0; elim x0; intros; split; left; assumption.
+  apply derive_pt_eq_0; apply H0; elim P; intros; split; left; assumption.
   apply derive_pt_eq_0; apply derivable_pt_lim_id.
   assumption.
   intros; apply derivable_continuous_pt; apply X1; assumption.
@@ -217,12 +217,12 @@ Proof.
   assert (H3 := MVT f id a b pr H2 H0 H);
     assert (H4 : forall x:R, a <= x <= b -> continuity_pt id x).
   intros; apply derivable_continuous; apply derivable_id.
-  elim (H3 H4); intros; elim H5; intros; exists x; exists x0; rewrite H1 in H6;
-    unfold id in H6; unfold Rminus in H6; rewrite Rplus_opp_r in H6;
-      rewrite Rmult_0_l in H6; apply Rmult_eq_reg_l with (b - a);
-        [ rewrite Rmult_0_r; apply H6
-          | apply Rminus_eq_contra; red; intro; rewrite H7 in H0;
-            elim (Rlt_irrefl _ H0) ].
+  destruct (H3 H4) as (c & P & H6). exists c; exists P; rewrite H1 in H6.
+  unfold id in H6; unfold Rminus in H6; rewrite Rplus_opp_r in H6.
+  rewrite Rmult_0_l in H6; apply Rmult_eq_reg_l with (b - a);
+    [ rewrite Rmult_0_r; apply H6
+      | apply Rminus_eq_contra; red; intro H7; rewrite H7 in H0;
+        elim (Rlt_irrefl _ H0) ].
 Qed.
 
 (**********)
@@ -655,14 +655,15 @@ Proof.
   elim H1; intros; apply Rle_trans with x; assumption.
   elim H1; clear H1; intros; elim H1; clear H1; intro.
   assert (H7 := MVT f id a x H4 H2 H1 H5 H3).
-  elim H7; intros; elim H8; intros; assert (H10 : a < x0 < b).
-  elim x1; intros; split.
-  assumption.
-  apply Rlt_le_trans with x; assumption.
-  assert (H11 : derive_pt f x0 (H4 x0 x1) = 0).
-  replace (derive_pt f x0 (H4 x0 x1)) with (derive_pt f x0 (pr x0 H10));
+  destruct H7 as (c & P & H9).
+  assert (H10 : a < c < b).
+  split.
+  apply P.
+  apply Rlt_le_trans with x; [apply P|assumption].
+  assert (H11 : derive_pt f c (H4 c P) = 0).
+  replace (derive_pt f c (H4 c P)) with (derive_pt f c (pr c H10));
   [ apply H0 | apply pr_nu ].
-  assert (H12 : derive_pt id x0 (H2 x0 x1) = 1).
+  assert (H12 : derive_pt id c (H2 c P) = 1).
   apply derive_pt_eq_0; apply derivable_pt_lim_id.
   rewrite H11 in H9; rewrite H12 in H9; rewrite Rmult_0_r in H9;
     rewrite Rmult_1_r in H9; apply Rminus_diag_uniq; symmetry ;
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;