diff options
Diffstat (limited to 'theories/Numbers/Integer/BigZ/BigZ.v')
| -rw-r--r-- | theories/Numbers/Integer/BigZ/BigZ.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v index 443777f5..a56f90b0 100644 --- a/theories/Numbers/Integer/BigZ/BigZ.v +++ b/theories/Numbers/Integer/BigZ/BigZ.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -76,7 +76,7 @@ Infix "รท" := BigZ.quot (at level 40, left associativity) : bigZ_scope. (** Some additional results about [BigZ] *) Theorem spec_to_Z: forall n : bigZ, - BigN.to_Z (BigZ.to_N n) = ((Zsgn [n]) * [n])%Z. + BigN.to_Z (BigZ.to_N n) = ((Z.sgn [n]) * [n])%Z. Proof. intros n; case n; simpl; intros p; generalize (BigN.spec_pos p); case (BigN.to_Z p); auto. @@ -85,7 +85,7 @@ intros p1 H1; case H1; auto. Qed. Theorem spec_to_N n: - ([n] = Zsgn [n] * (BigN.to_Z (BigZ.to_N n)))%Z. + ([n] = Z.sgn [n] * (BigN.to_Z (BigZ.to_N n)))%Z. Proof. case n; simpl; intros p; generalize (BigN.spec_pos p); case (BigN.to_Z p); auto. @@ -118,7 +118,7 @@ Qed. Lemma BigZeqb_correct : forall x y, (x =? y) = true -> x==y. Proof. now apply BigZ.eqb_eq. Qed. -Definition BigZ_of_N n := BigZ.of_Z (Z_of_N n). +Definition BigZ_of_N n := BigZ.of_Z (Z.of_N n). Lemma BigZpower : power_theory 1 BigZ.mul BigZ.eq BigZ_of_N BigZ.pow. Proof. @@ -139,7 +139,7 @@ BigZ.zify. auto with zarith. intros NEQ. generalize (BigZ.spec_div_eucl a b). generalize (Z_div_mod_full [a] [b] NEQ). -destruct BigZ.div_eucl as (q,r), Zdiv_eucl as (q',r'). +destruct BigZ.div_eucl as (q,r), Z.div_eucl as (q',r'). intros (EQ,_). injection 1. intros EQr EQq. BigZ.zify. rewrite EQr, EQq; auto. Qed. |