| Commit message (Collapse) | Author | Age |
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
| |
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
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10313 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
| |
that aren't so nice after all. For instance, ((a+b*c) mod c) might differ
from (a mod c), due to sign issues.
Minor improvements to Zdiv
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10312 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10307 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
A file ZOdiv is added which contains results about this euclidean division.
Interest compared with Zdiv: ZOdiv implements others (better?) conventions
concerning negative numbers, in particular it is compatible with Caml
div and mod.
ZOdiv is only partially finished...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10302 85f007b7-540e-0410-9357-904b9bb8a0f7
|