proposition: Theorem Rnd_UP_pt_monotone : forall F : R -> Prop, round_pred_monotone (Rnd_UP_pt F).
proof: Proof. intros F x y f g (Hx1,(_,Hx2)) (Hy1,(Hy2,_)) Hxy. apply Hx2. apply Hy1. now apply Rle_trans with (1 := Hxy). Qed.
imports: Coq(Reals) Raux Defs