diff options
| -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 53d78d3b73..e11194a5d9 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; |