diff options
Diffstat (limited to 'theories/Numbers/Integer/Abstract/ZPlusOrder.v')
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZPlusOrder.v | 21 |
1 files changed, 21 insertions, 0 deletions
diff --git a/theories/Numbers/Integer/Abstract/ZPlusOrder.v b/theories/Numbers/Integer/Abstract/ZPlusOrder.v index ce79055a7..c6d0efe45 100644 --- a/theories/Numbers/Integer/Abstract/ZPlusOrder.v +++ b/theories/Numbers/Integer/Abstract/ZPlusOrder.v @@ -89,6 +89,27 @@ Proof NZplus_nonneg_cases. (** Theorems that are either not valid on N or have different proofs on N and Z *) +Theorem Zplus_neg_neg : forall n m : Z, n < 0 -> m < 0 -> n + m < 0. +Proof. +intros n m H1 H2. rewrite <- (Zplus_0_l 0). now apply Zplus_lt_mono. +Qed. + +Theorem Zplus_neg_nonpos : forall n m : Z, n < 0 -> m <= 0 -> n + m < 0. +Proof. +intros n m H1 H2. rewrite <- (Zplus_0_l 0). now apply Zplus_lt_le_mono. +Qed. + +Theorem Zplus_nonpos_neg : forall n m : Z, n <= 0 -> m < 0 -> n + m < 0. +Proof. +intros n m H1 H2. rewrite <- (Zplus_0_l 0). now apply Zplus_le_lt_mono. +Qed. + +Theorem Zplus_nonpos_nonpos : forall n m : Z, n <= 0 -> m <= 0 -> n + m <= 0. +Proof. +intros n m H1 H2. rewrite <- (Zplus_0_l 0). now apply Zplus_le_mono. +Qed. + + (** Minus and order *) Theorem Zlt_lt_minus : forall n m : Z, n < m <-> 0 < m - n. |