From e1cad068ffc188d06c37f46e1bf6e7b57e02e219 Mon Sep 17 00:00:00 2001 From: letouzey Date: Fri, 17 Dec 2010 21:00:26 +0000 Subject: 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 --- theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'theories/Numbers/Natural/SpecViaZ') 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. -- cgit v1.2.3