proposition: Theorem Rnd_NA_pt_monotone : forall F : R -> Prop, F 0 -> round_pred_monotone (Rnd_NA_pt F).
proof: Proof. intros F HF x y f g Hxf Hyg Hxy. apply (Rnd_NG_pt_monotone F _ (Rnd_NA_pt_unique_prop F HF) x y). now apply -> Rnd_NA_NG_pt. now apply -> Rnd_NA_NG_pt. exact Hxy. Qed.
imports: Coq(Reals) Raux Defs