diff options
| author | emakarov | 2007-10-16 16:28:17 +0000 |
|---|---|---|
| committer | emakarov | 2007-10-16 16:28:17 +0000 |
| commit | d7e249dc1bfc2dd04ccf23c57b7ad40f1902568d (patch) | |
| tree | 543ff4b9aee9cb17b6d3f2239cbc1f6a3e931929 /theories/Numbers/Integer/Abstract/ZTimesOrder.v | |
| parent | 201def788a3cac497134f460b90eb33bd5f80cce (diff) | |
Added transitivity and irreflexivity of <, as well as < -elimination for binary positive numbers.
Added directory contribs/micromega with the generalization of Frédéric Besson's micromega tactic for an arbitrary ordered ring. So far no tactic has been defined. One has to apply the theorems and find the certificate, which is necessary to solve inequations, manually.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10226 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Numbers/Integer/Abstract/ZTimesOrder.v')
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZTimesOrder.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/theories/Numbers/Integer/Abstract/ZTimesOrder.v b/theories/Numbers/Integer/Abstract/ZTimesOrder.v index d63dc0d8c6..4381420950 100644 --- a/theories/Numbers/Integer/Abstract/ZTimesOrder.v +++ b/theories/Numbers/Integer/Abstract/ZTimesOrder.v @@ -94,6 +94,9 @@ Theorem Ztimes_neg : forall n m : Z, n * m < 0 <-> (n < 0 /\ m > 0) \/ (n > 0 /\ m < 0). Proof NZtimes_neg. +Theorem Ztimes_2_mono_l : forall n m : Z, n < m -> 1 + (1 + 1) * n < (1 + 1) * m. +Proof NZtimes_2_mono_l. + (** Theorems that are either not valid on N or have different proofs on N and Z *) (* None? *) |