Cosmetic : let's take advantage of the n-ary exists notation

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13721 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 2 insertions, 2 deletions

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.