diff options
| author |  desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-01-21 16:07:12 +0000 |
|---|---|---|
| committer | desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-01-21 16:07:12 +0000 |
| commit | 3e4691892a6dd69c04fc4e3fd4b1188d7f9a504d (patch) | |
| tree | d904961027d5b1f336544c78437955a113e67f42 /theories/Reals/ArithProp.v | |
| parent | 92bac4d9048a189113469516744db34af82cc421 (diff) | |
MAJ ArithProp
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3559 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Reals/ArithProp.v')
| -rw-r--r-- | theories/Reals/ArithProp.v | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/theories/Reals/ArithProp.v b/theories/Reals/ArithProp.v index 1d467a111..3436a2558 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). |