diff options
Diffstat (limited to 'theories/Numbers/Integer/Abstract/ZAddOrder.v')
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZAddOrder.v | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/theories/Numbers/Integer/Abstract/ZAddOrder.v b/theories/Numbers/Integer/Abstract/ZAddOrder.v index eb27e63782..b5ca908b40 100644 --- a/theories/Numbers/Integer/Abstract/ZAddOrder.v +++ b/theories/Numbers/Integer/Abstract/ZAddOrder.v @@ -102,6 +102,11 @@ Proof. intro n. rewrite (opp_le_mono 0 n). now rewrite opp_0. Qed. +Theorem lt_m1_0 : -(1) < 0. +Proof. +apply opp_neg_pos, lt_0_1. +Qed. + Theorem sub_lt_mono_l : forall n m p, n < m <-> p - m < p - n. Proof. intros n m p. do 2 rewrite <- add_opp_r. rewrite <- add_lt_mono_l. |