proposition: Theorem Rnd_N_pt_refl : forall F : R -> Prop, forall x : R, F x -> Rnd_N_pt F x x.
proof: Proof. intros F x Hx. repeat split. exact Hx. intros g _. unfold Rminus at 1. rewrite Rplus_opp_r, Rabs_R0. apply Rabs_pos. Qed.
imports: Coq(Reals) Raux Defs