From cb24ec6fd2c79a317f98b7dad426ac3e9bbad56a Mon Sep 17 00:00:00 2001 From: emakarov Date: Fri, 16 Nov 2007 20:37:52 +0000 Subject: Added theorems; created NZPlusOrder from NTimesOrder. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10325 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Numbers/Integer/Abstract/ZLt.v | 28 ++++++++++++++++++++++++++++ 1 file changed, 28 insertions(+) (limited to 'theories/Numbers/Integer/Abstract/ZLt.v') diff --git a/theories/Numbers/Integer/Abstract/ZLt.v b/theories/Numbers/Integer/Abstract/ZLt.v index a81b3a419..27cbe085e 100644 --- a/theories/Numbers/Integer/Abstract/ZLt.v +++ b/theories/Numbers/Integer/Abstract/ZLt.v @@ -75,6 +75,12 @@ Proof NZlt_succ_diag_r. Theorem Zle_succ_diag_r : forall n : Z, n <= S n. Proof NZle_succ_diag_r. +Theorem Zlt_0_1 : 0 < 1. +Proof NZlt_0_1. + +Theorem Zle_0_1 : 0 <= 1. +Proof NZle_0_1. + Theorem Zlt_lt_succ_r : forall n m : Z, n < m -> n < S m. Proof NZlt_lt_succ_r. @@ -150,6 +156,28 @@ Proof NZlt_ge_cases. Theorem Zle_ge_cases : forall n m : Z, n <= m \/ n >= m. Proof NZle_ge_cases. +(** Instances of the previous theorems for m == 0 *) + +Theorem Zneg_pos_cases : forall n : Z, n ~= 0 <-> n < 0 \/ n > 0. +Proof. +intro; apply Zlt_gt_cases. +Qed. + +Theorem Znonpos_pos_cases : forall n : Z, n <= 0 \/ n > 0. +Proof. +intro; apply Zle_gt_cases. +Qed. + +Theorem Zneg_nonneg_cases : forall n : Z, n < 0 \/ n >= 0. +Proof. +intro; apply Zlt_ge_cases. +Qed. + +Theorem Znonpos_nonneg_cases : forall n : Z, n <= 0 \/ n >= 0. +Proof. +intro; apply Zle_ge_cases. +Qed. + Theorem Zle_ngt : forall n m : Z, n <= m <-> ~ n > m. Proof NZle_ngt. -- cgit v1.2.3