diff options
| author | letouzey | 2011-06-24 15:50:17 +0000 |
|---|---|---|
| committer | letouzey | 2011-06-24 15:50:17 +0000 |
| commit | ad0c122b1665fedde52f51ecdebb9d04a12831a6 (patch) | |
| tree | f19253819ee220024a38aa4509f01fe84adc4107 /theories/Numbers/Integer | |
| parent | 7e00447c512b71543cec6b6fd63ec44106dada3d (diff) | |
Clean-up of Znumtheory, deletion of Zgcd_def
In particular, we merge the old Zdivide (used to be an ad-hoc
inductive predicate) and the new Z.divide (based on exists).
Notations allow to do that (almost) transparently, the only
impact is that the name picked by the system will not be "q"
anymore when destructing a Z.divide. Some fragile scripts
may have to be fixed.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14239 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Numbers/Integer')
| -rw-r--r-- | theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v index 44dd2c5934..6facd3c3a6 100644 --- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v +++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v @@ -421,22 +421,22 @@ Qed. Lemma gcd_divide_l : forall n m, (gcd n m | n). Proof. - intros n m. apply spec_divide. zify. apply Zgcd_divide_l. + intros n m. apply spec_divide. zify. apply Z.gcd_divide_l. Qed. Lemma gcd_divide_r : forall n m, (gcd n m | m). Proof. - intros n m. apply spec_divide. zify. apply Zgcd_divide_r. + intros n m. apply spec_divide. zify. apply Z.gcd_divide_r. Qed. Lemma gcd_greatest : forall n m p, (p|n) -> (p|m) -> (p|gcd n m). Proof. - intros n m p. rewrite !spec_divide. zify. apply Zgcd_greatest. + intros n m p. rewrite !spec_divide. zify. apply Z.gcd_greatest. Qed. Lemma gcd_nonneg : forall n m, 0 <= gcd n m. Proof. - intros. zify. apply Zgcd_nonneg. + intros. zify. apply Z.gcd_nonneg. Qed. (** Bitwise operations *) |