diff options
Diffstat (limited to 'theories/Numbers/Integer/Abstract/ZOrder.v')
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZOrder.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/theories/Numbers/Integer/Abstract/ZOrder.v b/theories/Numbers/Integer/Abstract/ZOrder.v index 295f5355a..e0ef2f15d 100644 --- a/theories/Numbers/Integer/Abstract/ZOrder.v +++ b/theories/Numbers/Integer/Abstract/ZOrder.v @@ -23,6 +23,9 @@ Proof NZlt_le_incl. Theorem Zlt_neq : forall n m : Z, n < m -> n ~= m. Proof NZlt_neq. +Theorem Zlt_le_neq : forall n m : Z, n < m <-> n <= m /\ n ~= m. +Proof NZlt_le_neq. + Theorem Zle_refl : forall n : Z, n <= n. Proof NZle_refl. |