7 files changed, 9 insertions, 9 deletions
diff --git a/theories/Numbers/Integer/Abstract/ZGcd.v b/theories/Numbers/Integer/Abstract/ZGcd.v
index 8e128215d..77a7c7341 100644
--- a/theories/Numbers/Integer/Abstract/ZGcd.v
+++ b/theories/Numbers/Integer/Abstract/ZGcd.v
@@ -141,7 +141,7 @@ Proof.
  rewrite <- add_opp_r, <- mul_opp_l. apply gcd_add_mult_diag_r.
 Qed.
 
-Definition Bezout n m p := exists a, exists b, a*n + b*m == p.
+Definition Bezout n m p := exists a b, a*n + b*m == p.
 
 Instance Bezout_wd : Proper (eq==>eq==>eq==>iff) Bezout.
 Proof.
@@ -250,7 +250,7 @@ Proof.
 Qed.
 
 Lemma divide_mul_split : forall n m p, n ~= 0 -> (n | m * p) ->
- exists q, exists r, n == q*r /\ (q | m) /\ (r | p).
+ exists q r, n == q*r /\ (q | m) /\ (r | p).
 Proof.
  intros n m p Hn H.
  assert (G := gcd_nonneg n m).
diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
index 8c1e7b4fa..2c46be4c7 100644
--- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
+++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
@@ -412,7 +412,7 @@ Qed.
 (** Bitwise operations *)
 
 Lemma testbit_spec : forall a n, 0<=n ->
-  exists l, exists h, (0<=l /\ l<2^n) /\
+  exists l h, (0<=l /\ l<2^n) /\
     a == l + ((if testbit a n then 1 else 0) + 2*h)*2^n.
 Proof.
  intros a n. zify. intros H.
diff --git a/theories/Numbers/NatInt/NZBits.v b/theories/Numbers/NatInt/NZBits.v
index 072daa273..a7539bc99 100644
--- a/theories/Numbers/NatInt/NZBits.v
+++ b/theories/Numbers/NatInt/NZBits.v
@@ -42,7 +42,7 @@ Module Type NZBitsSpec
  (Import A : NZOrdAxiomsSig')(Import B : Pow' A)(Import C : Bits' A).
 
  Axiom testbit_spec : forall a n, 0<=n ->
-  exists l, exists h, 0<=l<2^n /\
+  exists l h, 0<=l<2^n /\
     a == l + ((if a.[n] then 1 else 0) + 2*h)*2^n.
  Axiom testbit_neg_r : forall a n, n<0 -> a.[n] = false.
 
diff --git a/theories/Numbers/NatInt/NZDomain.v b/theories/Numbers/NatInt/NZDomain.v
index 2ab7413e3..9c01ba8cd 100644
--- a/theories/Numbers/NatInt/NZDomain.v
+++ b/theories/Numbers/NatInt/NZDomain.v
@@ -59,7 +59,7 @@ Module NZDomainProp (Import NZ:NZDomainSig').
 
 (** We prove that any points in NZ have a common descendant by [succ] *)
 
-Definition common_descendant n m := exists k, exists l, (S^k) n == (S^l) m.
+Definition common_descendant n m := exists k l, (S^k) n == (S^l) m.
 
 Instance common_descendant_wd : Proper (eq==>eq==>iff) common_descendant.
 Proof.
diff --git a/theories/Numbers/Natural/Abstract/NGcd.v b/theories/Numbers/Natural/Abstract/NGcd.v
index 77f23a02b..1340e5124 100644
--- a/theories/Numbers/Natural/Abstract/NGcd.v
+++ b/theories/Numbers/Natural/Abstract/NGcd.v
@@ -72,7 +72,7 @@ Qed.
 (** On natural numbers, we should use a particular form
   for the Bezout identity, since we don't have full subtraction. *)
 
-Definition Bezout n m p := exists a, exists b, a*n == p + b*m.
+Definition Bezout n m p := exists a b, a*n == p + b*m.
 
 Instance Bezout_wd : Proper (eq==>eq==>eq==>iff) Bezout.
 Proof.
@@ -188,7 +188,7 @@ Proof.
 Qed.
 
 Lemma divide_mul_split : forall n m p, n ~= 0 -> (n | m * p) ->
- exists q, exists r, n == q*r /\ (q | m) /\ (r | p).
+ exists q r, n == q*r /\ (q | m) /\ (r | p).
 Proof.
  intros n m p Hn H.
  assert (G := gcd_nonneg n m).
diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v
index 2802e42be..277223f4b 100644
--- a/theories/Numbers/Natural/Peano/NPeano.v
+++ b/theories/Numbers/Natural/Peano/NPeano.v
@@ -404,7 +404,7 @@ Proof.
 Qed.
 
 Lemma testbit_spec : forall a n,
- exists l, exists h, 0<=l<2^n /\
+ exists l h, 0<=l<2^n /\
   a = l + ((if testbit a n then 1 else 0) + 2*h)*2^n.
 Proof.
  intros a n. revert a. induction n; intros a; simpl testbit.
diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
index 175b1ad2c..8ee48ba55 100644
--- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
+++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
@@ -338,7 +338,7 @@ Qed.
 (** Bitwise operations *)
 
 Lemma testbit_spec : forall a n, 0<=n ->
-  exists l, exists h, (0<=l /\ l<2^n) /\
+  exists l h, (0<=l /\ l<2^n) /\
     a == l + ((if testbit a n then 1 else 0) + 2*h)*2^n.
 Proof.
  intros a n _. zify.