diff --git a/Lebesgue/UniformSpace_compl.v b/Lebesgue/UniformSpace_compl.v
index c6df32bd9a77505c37cd8f48f03c6037e6086c06..e956f3e80e5bcb0db1212ca302fe5bed0d00ccf4 100644
--- a/Lebesgue/UniformSpace_compl.v
+++ b/Lebesgue/UniformSpace_compl.v
@@ -354,9 +354,6 @@ Qed.
 Lemma filterlim_Rloc_seq_r :
   forall x, filterlim (Rloc_seq_r x) eventually (at_right x).
 Proof.
-assert (InvINRp1_pos : forall n : nat, 0 < / (INR n + 1)).
-intros n; apply Rinv_0_lt_compat, INRp1_pos.
-(* *)
 intros x.
 intros P [alpha H].
 unfold Rloc_seq_r.