Deux petits théorèmes utiles dans Minus.v

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10401 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 27 insertions, 10 deletions

diff --git a/theories/Arith/Minus.v b/theories/Arith/Minus.v
index 0bbed2789..8a62eb88b 100644
--- a/theories/Arith/Minus.v
+++ b/theories/Arith/Minus.v
@@ -97,23 +97,40 @@ Hint Resolve le_plus_minus_r: arith v62.
 
 (** * Relation with order *)
 
-Theorem le_minus : forall n m, n - m <= n.
+Theorem minus_le_compat_r : forall n m p : nat, n <= m -> n - p <= m - p.
 Proof.
-  intros i h; pattern i, h in |- *; apply nat_double_ind;
-    [ auto
-      | auto
-      | intros m n H; simpl in |- *; apply le_trans with (m := m); auto ].
+  intros n m p; generalize n m; clear n m; induction p as [|p HI].
+    intros n m; rewrite <- (minus_n_O n); rewrite <- (minus_n_O m); trivial.
+
+    intros n m Hnm; apply le_elim_rel with (n:=n) (m:=m); auto with arith.
+    intros q r H _. simpl. auto using HI.
+Qed.
+
+Theorem minus_le_compat_l : forall n m p : nat, n <= m -> p - m <= p - n.
+Proof.
+  intros n m p; generalize n m; clear n m; induction p as [|p HI].
+    trivial.
+
+    intros n m Hnm; apply le_elim_rel with (n:=n) (m:=m); trivial.
+      intros q; destruct q; auto with arith.
+        simpl. 
+        apply le_trans with (m := p - 0); [apply HI | rewrite <- minus_n_O];
+          auto with arith.
+        
+      intros q r Hqr _. simpl. auto using HI.
 Qed.
 
+Corollary le_minus : forall n m, n - m <= n.
+Proof.
+  intros n m; rewrite minus_n_O; auto using minus_le_compat_l with arith.
+Qed.
+Hint Resolve le_minus: arith v62.
+
 Lemma lt_minus : forall n m, m <= n -> 0 < m -> n - m < n.
 Proof.
   intros n m Le; pattern m, n in |- *; apply le_elim_rel; simpl in |- *;
     auto with arith.
-  intros; absurd (0 < 0); auto with arith.
-  intros p q lepq Hp gtp.
-  elim (le_lt_or_eq 0 p); auto with arith.
-  auto with arith.
-  induction 1; elim minus_n_O; auto with arith.
+    intros; absurd (0 < 0); auto with arith.
 Qed.
 Hint Resolve lt_minus: arith v62.