From c981c0974e76eab39d916f79374b6432cf188558 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 11 Mar 2004 22:33:52 +0000
Subject: Ajout d'un vieil exemple de N. Magaud

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5457 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/success/eauto.v | 13 ++++++++++++-
 1 file changed, 12 insertions(+), 1 deletion(-)

diff --git a/test-suite/success/eauto.v b/test-suite/success/eauto.v
index 8a5e146d4e..999cb1212a 100644
--- a/test-suite/success/eauto.v
+++ b/test-suite/success/eauto.v
@@ -33,6 +33,17 @@ Intros.
 EAuto with essai.
 Save.
 
+(* Example from Nicolas Magaud on coq-club - Jul 2000 *)
 
+Definition Nat: Set := nat.
+Parameter S':Nat ->Nat.
+Parameter plus':Nat -> Nat ->Nat.
 
-
+Lemma simpl_plus_l_rr1:
+  ((n0:Nat) ((m, p:Nat) (plus' n0 m)=(plus' n0 p) ->m=p) ->
+   (m, p:Nat) (S' (plus' n0 m))=(S' (plus' n0 p)) ->m=p) ->
+  (n:Nat) ((m, p:Nat) (plus' n m)=(plus' n p) ->m=p) ->
+  (m, p:Nat) (S' (plus' n m))=(S' (plus' n p)) ->m=p.
+Intros.
+EAuto. (* does EApply H *) 
+Qed.
-- 
cgit v1.2.3