diff options
| author | herbelin | 2003-09-25 19:58:49 +0000 |
|---|---|---|
| committer | herbelin | 2003-09-25 19:58:49 +0000 |
| commit | 5bb42bbdb310392825d075dab81591463a871a1a (patch) | |
| tree | a41e3a47f5b3fbc46071141a404aa9f1aba6cd8c | |
| parent | d2f991121cfdd721e3e5a8b3db5518c46c0f8f57 (diff) | |
add_x_x de fast_integer vers auxiliary
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4475 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | theories/ZArith/auxiliary.v | 6 |
1 files changed, 1 insertions, 5 deletions
diff --git a/theories/ZArith/auxiliary.v b/theories/ZArith/auxiliary.v index 68a5237839..ec8b42ac71 100644 --- a/theories/ZArith/auxiliary.v +++ b/theories/ZArith/auxiliary.v @@ -17,6 +17,7 @@ Require Decidable. Require Peano_dec. Require Export Compare_dec. + Definition neq := [x,y:nat] ~(x=y). Definition Zne := [x,y:Z] ~(x=y). Theorem add_un_Zs : (x:positive) (POS (add_un x)) = (Zs (POS x)). @@ -334,11 +335,6 @@ Intros r x y z t; Case r; [ Rewrite Zcompare_Zplus_compatible; Assumption]]. Qed. -Lemma add_x_x : (x:positive) (add x x) = (xO x). -Intros p; Apply convert_intro; Simpl; Rewrite convert_add; -Unfold 3 convert ; Simpl; Rewrite ZL6; Trivial with arith. -Qed. - Theorem Zcompare_Zmult_compatible : (x:positive)(y,z:Z) (Zcompare (Zmult (POS x) y) (Zmult (POS x) z)) = (Zcompare y z). |