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