From e542de6a7f8e618c3f7f3997696e91774c50a3f9 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 14 Nov 2003 13:47:35 +0000
Subject: Backtrack sur Peano

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4902 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Init/Peano.v | 12 ------------
 1 file changed, 12 deletions(-)

diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v
index d521a845d5..2356c9cb59 100755
--- a/theories/Init/Peano.v
+++ b/theories/Init/Peano.v
@@ -119,24 +119,12 @@ Hint eq_mult : core v62 := Resolve (f_equal2 nat nat nat mult).
 
 V8Infix "*" mult : nat_scope.
 
-Lemma mult_O_r : (n:nat) (mult n O)=O.
-Proof.
-  NewInduction n; Simpl; Auto.
-Qed.
-
 Lemma mult_n_O : (n:nat) O=(mult n O).
 Proof.
   NewInduction n; Simpl; Auto.
 Qed.
 Hints Resolve mult_n_O : core v62.
 
-Lemma mult_S_r : (n,m:nat) (mult n (S m))=(plus (mult n m) n).
-Proof.
-  Intros; NewInduction n as [|p H]; Simpl; Auto.
-  Rewrite H; Rewrite <- plus_n_Sm; Apply (f_equal nat nat S).
-  Pattern 1 3 m; Elim m; Simpl; Auto.
-Qed.
-
 Lemma mult_n_Sm : (n,m:nat) (plus (mult n m) n)=(mult n (S m)).
 Proof.
   Intros; NewInduction n as [|p H]; Simpl; Auto.
-- 
cgit v1.2.3