From 97fefe1fcca363a1317e066e7f4b99b9c1e9987b Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Thu, 12 Jan 2012 16:02:20 +0100
Subject: Imported Upstream version 8.4~beta

---
 theories/Numbers/Natural/Abstract/NSub.v | 44 ++++++++++++++++++++++----------
 1 file changed, 31 insertions(+), 13 deletions(-)

(limited to 'theories/Numbers/Natural/Abstract/NSub.v')

diff --git a/theories/Numbers/Natural/Abstract/NSub.v b/theories/Numbers/Natural/Abstract/NSub.v
index c0be3114..d7143c67 100644
--- a/theories/Numbers/Natural/Abstract/NSub.v
+++ b/theories/Numbers/Natural/Abstract/NSub.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -8,12 +8,10 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i $Id: NSub.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 Require Export NMulOrder.
 
-Module Type NSubPropFunct (Import N : NAxiomsSig').
-Include NMulOrderPropFunct N.
+Module Type NSubProp (Import N : NAxiomsMiniSig').
+Include NMulOrderProp N.
 
 Theorem sub_0_l : forall n, 0 - n == 0.
 Proof.
@@ -37,7 +35,7 @@ Qed.
 Theorem sub_gt : forall n m, n > m -> n - m ~= 0.
 Proof.
 intros n m H; elim H using lt_ind_rel; clear n m H.
-solve_relation_wd.
+solve_proper.
 intro; rewrite sub_0_r; apply neq_succ_0.
 intros; now rewrite sub_succ.
 Qed.
@@ -47,8 +45,8 @@ Proof.
 intros n m p; induct p.
 intro; now do 2 rewrite sub_0_r.
 intros p IH H. do 2 rewrite sub_succ_r.
-rewrite <- IH by (apply lt_le_incl; now apply -> le_succ_l).
-rewrite add_pred_r by (apply sub_gt; now apply -> le_succ_l).
+rewrite <- IH by (apply lt_le_incl; now apply le_succ_l).
+rewrite add_pred_r by (apply sub_gt; now apply le_succ_l).
 reflexivity.
 Qed.
 
@@ -205,6 +203,26 @@ Proof.
 intros n m p. rewrite add_comm; apply lt_add_lt_sub_r.
 Qed.
 
+Theorem sub_lt : forall n m, m <= n -> 0 < m -> n - m < n.
+Proof.
+intros n m LE LT.
+assert (LE' := le_sub_l n m). rewrite lt_eq_cases in LE'.
+destruct LE' as [LT'|EQ]. assumption.
+apply add_sub_eq_nz in EQ; [|order].
+rewrite (add_lt_mono_r _ _ n), add_0_l in LT. order.
+Qed.
+
+Lemma sub_le_mono_r : forall n m p, n <= m -> n-p <= m-p.
+Proof.
+ intros. rewrite le_sub_le_add_r. transitivity m. assumption. apply sub_add_le.
+Qed.
+
+Lemma sub_le_mono_l : forall n m p, n <= m -> p-m <= p-n.
+Proof.
+ intros. rewrite le_sub_le_add_r.
+ transitivity (p-n+n); [ apply sub_add_le | now apply add_le_mono_l].
+Qed.
+
 (** Sub and mul *)
 
 Theorem mul_pred_r : forall n m, n * (P m) == n * m - n.
@@ -224,10 +242,10 @@ intros n IH. destruct (le_gt_cases m n) as [H | H].
 rewrite sub_succ_l by assumption. do 2 rewrite mul_succ_l.
 rewrite (add_comm ((n - m) * p) p), (add_comm (n * p) p).
 rewrite <- (add_sub_assoc p (n * p) (m * p)) by now apply mul_le_mono_r.
-now apply <- add_cancel_l.
-assert (H1 : S n <= m); [now apply <- le_succ_l |].
-setoid_replace (S n - m) with 0 by now apply <- sub_0_le.
-setoid_replace ((S n * p) - m * p) with 0 by (apply <- sub_0_le; now apply mul_le_mono_r).
+now apply add_cancel_l.
+assert (H1 : S n <= m); [now apply le_succ_l |].
+setoid_replace (S n - m) with 0 by now apply sub_0_le.
+setoid_replace ((S n * p) - m * p) with 0 by (apply sub_0_le; now apply mul_le_mono_r).
 apply mul_0_l.
 Qed.
 
@@ -298,5 +316,5 @@ Theorem add_dichotomy :
   forall n m, (exists p, p + n == m) \/ (exists p, p + m == n).
 Proof. exact le_alt_dichotomy. Qed.
 
-End NSubPropFunct.
+End NSubProp.
 
-- 
cgit v1.2.3