proposition: Fact ex6 : F 0 -> round_pred_monotone (Rnd_ZR_pt F).
proof: Proof. intros F0 x y f g [HPf HNf] [HPg HNg] xLy. destruct (Rle_lt_dec 0 x) as [xPos | xNPos]; destruct (Rle_lt_dec 0 y) as [yPos | yNPos]; try lra. - apply (ex2 x y); auto. - assert (xNeg : x <= 0) by lra. assert (f <= 0). destruct (HNf xNeg) as [_ [_ H1f]]. apply H1f; auto. assert (0 <= g). destruct (HPg yPos) as [_ [_ H1g]]. apply H1g; auto. lra. - assert (xNeg : x <= 0) by lra. assert (yNeg : y <= 0) by lra. apply (ex4 x y); auto. Qed.
imports: Psatz Reals Flocq(Core)