From 0b05b8de1bcb0716e1c6b19d265027da36b1c3cc Mon Sep 17 00:00:00 2001
From: letouzey
Date: Mon, 12 Mar 2007 17:11:32 +0000
Subject: Proof simplification for eq_nat_dec et le_lt_dec: induction over 2nd
 arg m can simply be a destruct. This helps (vm_)compute __a lot__.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9698 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Arith/Compare_dec.v | 2 +-
 theories/Arith/Peano_dec.v   | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'theories')

diff --git a/theories/Arith/Compare_dec.v b/theories/Arith/Compare_dec.v
index ce54239f92..8b7e2c61d1 100644
--- a/theories/Arith/Compare_dec.v
+++ b/theories/Arith/Compare_dec.v
@@ -34,7 +34,7 @@ Defined.
 Definition le_lt_dec n m : {n <= m} + {m < n}.
   induction n.
   auto with arith.
-  induction m.
+  destruct m.
   auto with arith.
   elim (IHn m); auto with arith.
 Defined.
diff --git a/theories/Arith/Peano_dec.v b/theories/Arith/Peano_dec.v
index 5a9e980738..42335f98ba 100644
--- a/theories/Arith/Peano_dec.v
+++ b/theories/Arith/Peano_dec.v
@@ -23,7 +23,7 @@ Defined.
 
 Theorem eq_nat_dec : forall n m, {n = m} + {n <> m}.
 Proof.
-  induction n; induction m; auto.
+  induction n; destruct m; auto.
   elim (IHn m); auto.
 Defined.
 
-- 
cgit v1.2.3