diff --git a/src/Core/Fcore_rnd.v b/src/Core/Fcore_rnd.v
index dfb14bf30c4b7cc4d6125f5fae82c900301cd7a1..baae3c3f63ce088832c224d9566c14c1636fccd9 100644
--- a/src/Core/Fcore_rnd.v
+++ b/src/Core/Fcore_rnd.v
@@ -724,6 +724,18 @@ rewrite <- Hxy in Hg, Hy.
 eapply Rnd_NG_pt_unicity ; try split ; eassumption.
 Qed.
 
+Theorem Rnd_NG_pt_refl :
+  forall (F : R -> Prop) (P : R -> R -> Prop),
+  forall x, F x -> Rnd_NG_pt F P x x.
+Proof.
+intros F P x Hx.
+split.
+now apply Rnd_N_pt_refl.
+right.
+intros f2 Hf2.
+now apply Rnd_N_pt_idempotent with F.
+Qed.
+
 Theorem Rnd_NG_pt_sym :
   forall (F : R -> Prop) (P : R -> R -> Prop),
   ( forall x, F x -> F (-x) ) ->