diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-06-28 23:30:10 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-06-28 23:30:10 +0000 |
commit | a0b31c88aa2bcd50524cbc48d16eb78c62da3445 (patch) | |
tree | ebf4533e46fb630e520a745f2b3df41d489a33ec /theories/Numbers/Cyclic | |
parent | 2941378aee6586bcff9f8a117f11e5c5c2327607 (diff) |
Deletion of useless Zsqrt_def
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14245 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Numbers/Cyclic')
-rw-r--r-- | theories/Numbers/Cyclic/ZModulo/ZModulo.v | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/theories/Numbers/Cyclic/ZModulo/ZModulo.v b/theories/Numbers/Cyclic/ZModulo/ZModulo.v index 3bdbca44a..d039fdcbf 100644 --- a/theories/Numbers/Cyclic/ZModulo/ZModulo.v +++ b/theories/Numbers/Cyclic/ZModulo/ZModulo.v @@ -574,15 +574,15 @@ Section ZModulo. generalize (Z_mod_lt [|x|] 2); omega. Qed. - Definition sqrt x := Zsqrt [|x|]. + Definition sqrt x := Z.sqrt [|x|]. Lemma spec_sqrt : forall x, [|sqrt x|] ^ 2 <= [|x|] < ([|sqrt x|] + 1) ^ 2. Proof. intros. unfold sqrt. repeat rewrite Zpower_2. - replace [|Zsqrt [|x|]|] with (Zsqrt [|x|]). - apply Zsqrt_spec; auto with zarith. + replace [|Z.sqrt [|x|]|] with (Z.sqrt [|x|]). + apply Z.sqrt_spec; auto with zarith. symmetry; apply Zmod_small. split. apply Z.sqrt_nonneg; auto. apply Zle_lt_trans with [|x|]; auto. @@ -594,7 +594,7 @@ Section ZModulo. match z with | Z0 => (0, C0 0) | Zpos p => - let (s,r) := Zsqrtrem (Zpos p) in + let (s,r) := Z.sqrtrem (Zpos p) in (s, if Z_lt_le_dec r wB then C0 r else C1 (r-wB)) | Zneg _ => (0, C0 0) end. @@ -610,8 +610,8 @@ Section ZModulo. remember ([|x|]*wB+[|y|]) as z. destruct z. auto with zarith. - generalize (Zsqrtrem_spec (Zpos p)). - destruct Zsqrtrem as (s,r); intros [U V]; auto with zarith. + generalize (Z.sqrtrem_spec (Zpos p)). + destruct Z.sqrtrem as (s,r); intros [U V]; auto with zarith. assert (s < wB). destruct (Z_lt_le_dec s wB); auto. assert (wB * wB <= Zpos p). |