diff options
-rw-r--r-- | theories/Reals/RIneq.v | 6 | ||||
-rw-r--r-- | theories/Reals/RiemannInt_SF.v | 2 |
2 files changed, 5 insertions, 3 deletions
diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v index 8b7cf3619..a6b481686 100644 --- a/theories/Reals/RIneq.v +++ b/theories/Reals/RIneq.v @@ -1311,12 +1311,14 @@ Hints Resolve not_1_INR : real. (** Injection from [Z] to [R] *) (**********************************************************) +V7only [ (**********) -Definition INZ:=inject_nat. +Notation INZ:=inject_nat. +]. (**********) Lemma IZN:(z:Z)(`0<=z`)->(Ex [n:nat] z=(INZ n)). -Unfold INZ;Intros;Apply inject_nat_complete;Assumption. +Intros;Apply inject_nat_complete;Assumption. Qed. (**********) 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)). |