From 3e4691892a6dd69c04fc4e3fd4b1188d7f9a504d Mon Sep 17 00:00:00 2001
From: desmettr
Date: Tue, 21 Jan 2003 16:07:12 +0000
Subject: MAJ ArithProp

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3559 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Reals/ArithProp.v | 1 -
 1 file changed, 1 deletion(-)

diff --git a/theories/Reals/ArithProp.v b/theories/Reals/ArithProp.v
index 1d467a1113..3436a2558c 100644
--- a/theories/Reals/ArithProp.v
+++ b/theories/Reals/ArithProp.v
@@ -47,7 +47,6 @@ Intros n m; Pattern n m; Apply nat_double_ind; [
 | Intros; Simpl; Apply H; Apply lt_S_n; Assumption].
 Qed.
 
-(* Tout entier s'ecrit sous la forme 2p ou 2p+1 *)
 Lemma even_odd_cor : (n:nat) (EX p : nat | n=(mult (2) p)\/n=(S (mult (2) p))).
 Intro.
 Assert H := (even_or_odd n).
-- 
cgit v1.2.3