diff options
| -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 68a523783..ec8b42ac7 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). |