diff options
| author | letouzey | 2009-09-09 16:10:59 +0000 |
|---|---|---|
| committer | letouzey | 2009-09-09 16:10:59 +0000 |
| commit | 8907c227f5c456f14617890946aa808ef522d7da (patch) | |
| tree | f8b9abbfb9f1713642fe5bf48d5ead64e4a5510c /theories/Numbers/Cyclic/ZModulo/ZModulo.v | |
| parent | e1723b1094719c1a60fddaa2668151b4f8ebc9ea (diff) | |
Znumtheory + Zdiv enriched with stuff from ZMicromega, misc improvements
Mostly results about Zgcd (commutativity, associativity, ...).
Slight improvement of ZMicromega.
Beware: some lemmas of Zdiv/ Znumtheory were asking for
too strict or useless hypothesis. Some minor glitches may occur.
By the way, some iff lemmas about negb in Bool.v
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12313 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Numbers/Cyclic/ZModulo/ZModulo.v')
| -rw-r--r-- | theories/Numbers/Cyclic/ZModulo/ZModulo.v | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/theories/Numbers/Cyclic/ZModulo/ZModulo.v b/theories/Numbers/Cyclic/ZModulo/ZModulo.v index b439462db3..7373acc9ad 100644 --- a/theories/Numbers/Cyclic/ZModulo/ZModulo.v +++ b/theories/Numbers/Cyclic/ZModulo/ZModulo.v @@ -546,7 +546,6 @@ Section ZModulo. apply Z_div_pos; auto with zarith. subst a; auto with zarith. apply Zdiv_lt_upper_bound; auto with zarith. - subst a; auto with zarith. subst a. replace (wB*[|b|]) with (([|b|]-1)*wB + wB) by ring. apply Zlt_le_trans with ([|a1|]*wB+wB); auto with zarith. |