aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Reals/RiemannInt_SF.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Reals/RiemannInt_SF.v')
-rw-r--r--theories/Reals/RiemannInt_SF.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Reals/RiemannInt_SF.v b/theories/Reals/RiemannInt_SF.v
index d4d25b112..1fc9811e5 100644
--- a/theories/Reals/RiemannInt_SF.v
+++ b/theories/Reals/RiemannInt_SF.v
@@ -23,7 +23,7 @@ Implicit Arguments On.
Definition Nbound [I:nat->Prop] : Prop := (EX n:nat | (i:nat)(I i)->(le i n)).
Lemma IZN_var:(z:Z)(`0<=z`)->{ n:nat | z=(INZ n)}.
-Unfold INZ;Intros; Apply inject_nat_complete_inf; Assumption.
+Intros; Apply inject_nat_complete_inf; Assumption.
Qed.
Lemma Nzorn : (I:nat->Prop) (EX n:nat | (I n)) -> (Nbound I) -> (sigTT ? [n:nat](I n)/\(i:nat)(I i)->(le i n)).