proposition: Fact ex2 : round_pred_monotone (Rnd_DN_pt F).
proof: Proof. intros x y f g Rxf Rxg xLy. destruct Rxf as [Ff [fLx fdown]]. destruct Rxg as [Fg [gLy gdown]]. apply gdown; try lra; assumption. Qed.
imports: Psatz Reals Flocq(Core)