diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-06-24 15:50:17 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-06-24 15:50:17 +0000 |
| commit | ad0c122b1665fedde52f51ecdebb9d04a12831a6 (patch) | |
| tree | f19253819ee220024a38aa4509f01fe84adc4107 /theories/Numbers/Cyclic | |
| 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/Cyclic')
| -rw-r--r-- | theories/Numbers/Cyclic/ZModulo/ZModulo.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/theories/Numbers/Cyclic/ZModulo/ZModulo.v b/theories/Numbers/Cyclic/ZModulo/ZModulo.v index 2d9eb395a..3bdbca44a 100644 --- a/theories/Numbers/Cyclic/ZModulo/ZModulo.v +++ b/theories/Numbers/Cyclic/ZModulo/ZModulo.v @@ -465,8 +465,8 @@ Section ZModulo. Proof. intros. generalize (Zgcd_is_gcd a b); inversion_clear 1. - destruct H2; destruct H3; clear H4. - assert (H3:=Zgcd_is_pos a b). + destruct H2 as (q,H2); destruct H3 as (q',H3); clear H4. + assert (H4:=Zgcd_is_pos a b). destruct (Z_eq_dec (Zgcd a b) 0). rewrite e; generalize (Zmax_spec a b); omega. assert (0 <= q). @@ -477,7 +477,7 @@ Section ZModulo. generalize (Zmax_spec 0 b) (Zabs_spec b); omega. apply Zle_trans with a. - rewrite H1 at 2. + rewrite H2 at 2. rewrite <- (Zmult_1_l (Zgcd a b)) at 1. apply Zmult_le_compat; auto with zarith. generalize (Zmax_spec a b); omega. |