From 62e7a0f9679f501f2bc9ff7343c8128a341da37c Mon Sep 17 00:00:00 2001
From: letouzey
Date: Thu, 3 Feb 2005 14:44:34 +0000
Subject: legere simplification des preuves de le_S_n et pred_le

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6669 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Arith/Le.v | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/theories/Arith/Le.v b/theories/Arith/Le.v
index b87f545a84..1f265b8f52 100755
--- a/theories/Arith/Le.v
+++ b/theories/Arith/Le.v
@@ -62,15 +62,14 @@ Hint Immediate le_Sn_le: arith v62.
 Theorem le_S_n : forall n m, S n <= S m -> n <= m.
 Proof.
 intros n m H; change (pred (S n) <= pred (S m)) in |- *.
-elim H; simpl in |- *; auto with arith.
+destruct H; simpl; auto with arith.
 Qed.
 Hint Immediate le_S_n: arith v62.
 
 Theorem le_pred : forall n m, n <= m -> pred n <= pred m.
 Proof.
-induction n as [| n IHn]. simpl in |- *. auto with arith.
-destruct m as [| m]. simpl in |- *. intro H. inversion H.
-simpl in |- *. auto with arith.
+destruct n; simpl; auto with arith.
+destruct m; simpl; auto with arith.
 Qed.
 
 (** Comparison to 0 *)
-- 
cgit v1.2.3