proposition: Theorem Rnd_N_pt_ge_0 : forall F : R -> Prop, F 0 -> forall x f, 0 <= x -> Rnd_N_pt F x f -> 0 <= f.
proof: Proof. intros F HF x f [Hx|Hx] Hxf. eapply Rnd_N_pt_monotone ; try eassumption. now apply Rnd_N_pt_0. right. apply sym_eq. apply Rnd_N_pt_idempotent with F. now rewrite Hx. exact HF. Qed.
imports: Coq(Reals) Raux Defs