diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-11-21 22:28:33 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-11-21 22:28:33 +0000 |
| commit | d7611cb4c5613f807b2c9fb5efb61b7663fcc4bd (patch) | |
| tree | e5dcac71dff627a90f70a945b792832110deff9c | |
| parent | 06eaa6883b276c3e14509ced57ef1e63f2ec21e4 (diff) | |
ajout Pnat (suite)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4963 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | theories/NArith/BinNat.v | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v index 53d78d3b7..e11194a5d 100644 --- a/theories/NArith/BinNat.v +++ b/theories/NArith/BinNat.v @@ -196,8 +196,6 @@ Qed. (** Properties of comparison *) -Require Pcompare. - Theorem Ncompare_Eq_eq : (n,m:entier) (Ncompare n m) = EGAL -> n = m. Proof. NewDestruct n as [|n]; NewDestruct m as [|m]; Simpl; Intro H; |