proposition: Theorem Rnd_NG_pt_monotone : forall (F : R -> Prop) (P : R -> R -> Prop), Rnd_NG_pt_unique_prop F P -> round_pred_monotone (Rnd_NG_pt F P).
proof: Proof. intros F P HP x y f g (Hf,Hx) (Hg,Hy) [Hxy|Hxy]. now apply Rnd_N_pt_monotone with F x y. apply Req_le. rewrite <- Hxy in Hg, Hy. eapply Rnd_NG_pt_unique ; try split ; eassumption. Qed.
imports: Coq(Reals) Raux Defs