proposition: Theorem Rnd_NA_pt_refl : forall F : R -> Prop, forall x : R, F x -> Rnd_NA_pt F x x.
proof: Proof. intros F x Hx. split. now apply Rnd_N_pt_refl. intros f Hxf. apply Req_le. apply f_equal. now apply Rnd_N_pt_idempotent with (1 := Hxf). Qed.
imports: Coq(Reals) Raux Defs