diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-06-24 15:50:06 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-06-24 15:50:06 +0000 |
| commit | 81c4c8bc418cdf42cc88249952dbba465068202c (patch) | |
| tree | 0151cc0964c9874722f237721b800076d08cef37 /theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v | |
| parent | 51c26ecf70212e6ec4130c41af9144058cd27d12 (diff) | |
Numbers: change definition of divide (compat with Znumtheory)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14237 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v')
| -rw-r--r-- | theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v index 878e46fea..33181e32a 100644 --- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v +++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v @@ -331,7 +331,7 @@ Qed. (** Gcd *) -Definition divide n m := exists p, n*p == m. +Definition divide n m := exists p, m == p*n. Local Notation "( x | y )" := (divide x y) (at level 0). Lemma spec_divide : forall n m, (n|m) <-> Z.divide [n] [m]. @@ -341,8 +341,8 @@ Proof. intros (z,H). exists (of_N (Zabs_N z)). zify. rewrite Z_of_N_abs. rewrite <- (Zabs_eq [n]) by apply spec_pos. - rewrite <- Zabs_Zmult, H. - apply Zabs_eq, spec_pos. + rewrite <- Zabs_Zmult, <- H. + symmetry. apply Zabs_eq, spec_pos. Qed. Lemma gcd_divide_l : forall n m, (gcd n m | n). |