(**
This file is part of the Flocq formalization of floating-point
arithmetic in Coq: http://flocq.gforge.inria.fr/

Copyright (C) 2010-2013 Sylvie Boldo
#<br />#
Copyright (C) 2010-2013 Guillaume Melquiond

This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
License as published by the Free Software Foundation; either
version 3 of the License, or (at your option) any later version.

This library is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
*)

(** * Roundings: properties and/or functions *)
Require Import Fcore_Raux.
Require Import Fcore_defs.

Section RND_prop.

Open Scope R_scope.

Theorem round_val_of_pred :
  forall rnd : R -> R -> Prop,
  round_pred rnd ->
  forall x, { f : R | rnd x f }.
Proof.
(* Goal: forall (rnd : forall (_ : R) (_ : R), Prop) (_ : round_pred rnd) (x : R), @sig R (fun f : R => rnd x f) *)
intros rnd (H1,H2) x.
(* Goal: @sig R (fun f : R => rnd x f) *)
specialize (H1 x).
(* . *)
(* Goal: @sig R (fun f : R => rnd x f) *)
assert (H3 : bound (rnd x)).
(* Goal: bound (rnd x) *)
(* Goal: @sig R (fun f : R => rnd x f) *)
destruct H1 as (f, H1).
(* Goal: @ex R (fun f : R => Rnd_NA_pt F x f) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
exists f.
(* Goal: forall (g : R) (_ : F g), Rle (Rabs (Rminus d x)) (Rabs (Rminus g x)) *)
(* Goal: or (P x d) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 d) *)
intros g Hg.
(* Goal: Rle f3 f2 *)
(* Goal: Rle f2 f1 *)
(* Goal: rnd x f1 *)
now apply H2 with (3 := Rle_refl x).
(* . *)
(* Goal: @sig R (fun f : R => rnd x f) *)
exists (proj1_sig (completeness _ H3 H1)).
(* Goal: rnd x (@proj1_sig R (fun m : R => is_lub (rnd x) m) (completeness (rnd x) H3 H1)) *)
destruct completeness as (f1, (H4, H5)).
(* Goal: rnd x (@proj1_sig R (fun m : R => is_lub (rnd x) m) (@exist R (fun m : R => is_lub (rnd x) m) f1 (@conj (is_upper_bound (rnd x) f1) (forall (b : R) (_ : is_upper_bound (rnd x) b), Rle f1 b) H4 H5))) *)
simpl.
(* Goal: rnd x f1 *)
destruct H1 as (f2, H1).
(* Goal: rnd x f1 *)
assert (f1 = f2).
(* Goal: @eq R (Rabs (Rminus f x)) (Rabs (Rminus g x)) *)
(* Goal: Rle (Rabs g) (Rabs f) *)
(* Goal: Rle (Rabs g) (Rabs f) *)
apply Rle_antisym.
(* Goal: Rle f1 f2 *)
(* Goal: Rle f2 f1 *)
(* Goal: rnd x f1 *)
apply H5.
(* Goal: is_upper_bound (rnd x) f2 *)
(* Goal: Rle f2 f1 *)
(* Goal: rnd x f1 *)
intros f3 H.
(* Goal: Rle f3 f2 *)
(* Goal: Rle f2 f1 *)
(* Goal: rnd x f1 *)
now apply H2 with (3 := Rle_refl x).
(* Goal: Rle f2 f1 *)
(* Goal: rnd x f1 *)
now apply H4.
(* Goal: rnd x f1 *)
now rewrite H.
Qed.

Theorem round_fun_of_pred :
  forall rnd : R -> R -> Prop,
  round_pred rnd ->
  { f : R -> R | forall x, rnd x (f x) }.
Proof.
(* Goal: forall (rnd : forall (_ : R) (_ : R), Prop) (_ : round_pred rnd), @sig (forall _ : R, R) (fun f : forall _ : R, R => forall x : R, rnd x (f x)) *)
intros rnd H.
(* Goal: @sig (forall _ : R, R) (fun f : forall _ : R, R => forall x : R, rnd x (f x)) *)
exists (fun x => proj1_sig (round_val_of_pred rnd H x)).
(* Goal: round_pred_total (Rnd_NA_pt F) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
intros x.
(* Goal: rnd x (@proj1_sig R (fun f : R => rnd x f) (round_val_of_pred rnd H x)) *)
now destruct round_val_of_pred as (f, H1).
Qed.

Theorem round_unicity :
  forall rnd : R -> R -> Prop,
  round_pred_monotone rnd ->
  forall x f1 f2,
  rnd x f1 ->
  rnd x f2 ->
  f1 = f2.
Proof.
(* Goal: forall (rnd : forall (_ : R) (_ : R), Prop) (_ : round_pred_monotone rnd) (x f1 f2 : R) (_ : rnd x f1) (_ : rnd x f2), @eq R f1 f2 *)
intros rnd Hr x f1 f2 H1 H2.
(* Goal: @eq R (Rabs (Rminus f x)) (Rabs (Rminus g x)) *)
(* Goal: Rle (Rabs g) (Rabs f) *)
(* Goal: Rle (Rabs g) (Rabs f) *)
apply Rle_antisym.
(* Goal: Rle f2 f1 *)
now apply Hr with (3 := Rle_refl x).
(* Goal: Rle f2 f1 *)
now apply Hr with (3 := Rle_refl x).
Qed.

Theorem Rnd_DN_pt_monotone :
  forall F : R -> Prop,
  round_pred_monotone (Rnd_DN_pt F).
Proof.
(* Goal: forall F : forall _ : R, Prop, round_pred_monotone (Rnd_DN_pt F) *)
intros F x y f g (Hx1,(Hx2,_)) (Hy1,(_,Hy2)) Hxy.
(* Goal: Rle f g *)
apply Hy2.
(* Goal: F f *)
(* Goal: Rle f y *)
apply Hx1.
(* Goal: Rle f y *)
now apply Rle_trans with (2 := Hxy).
Qed.

Theorem Rnd_DN_pt_unicity :
  forall F : R -> Prop,
  forall x f1 f2 : R,
  Rnd_DN_pt F x f1 -> Rnd_DN_pt F x f2 ->
  f1 = f2.
Proof.
(* Goal: forall (F : forall _ : R, Prop) (x f1 f2 : R) (_ : Rnd_UP_pt F x f1) (_ : Rnd_UP_pt F x f2), @eq R f1 f2 *)
intros F.
(* Goal: forall (x f1 f2 : R) (_ : Rnd_UP_pt F x f1) (_ : Rnd_UP_pt F x f2), @eq R f1 f2 *)
apply round_unicity.
(* Goal: round_pred_monotone (Rnd_DN_pt F) *)
apply Rnd_DN_pt_monotone.
Qed.

Theorem Rnd_DN_unicity :
  forall F : R -> Prop,
  forall rnd1 rnd2 : R -> R,
  Rnd_DN F rnd1 -> Rnd_DN F rnd2 ->
  forall x, rnd1 x = rnd2 x.
Proof.
(* Goal: forall (F : forall _ : R, Prop) (rnd1 rnd2 : forall _ : R, R) (_ : Rnd_UP F rnd1) (_ : Rnd_UP F rnd2) (x : R), @eq R (rnd1 x) (rnd2 x) *)
intros F rnd1 rnd2 H1 H2 x.
(* Goal: @eq R (rnd1 x) (rnd2 x) *)
now eapply Rnd_DN_pt_unicity.
Qed.

Theorem Rnd_UP_pt_monotone :
  forall F : R -> Prop,
  round_pred_monotone (Rnd_UP_pt F).
Proof.
(* Goal: forall F : forall _ : R, Prop, round_pred_monotone (Rnd_UP_pt F) *)
intros F x y f g (Hx1,(_,Hx2)) (Hy1,(Hy2,_)) Hxy.
(* Goal: Rle f g *)
apply Hx2.
(* Goal: Rle f g *)
(* Goal: Rle f g *)
apply Hy1.
(* Goal: Rle x g *)
now apply Rle_trans with (1 := Hxy).
Qed.

Theorem Rnd_UP_pt_unicity :
  forall F : R -> Prop,
  forall x f1 f2 : R,
  Rnd_UP_pt F x f1 -> Rnd_UP_pt F x f2 ->
  f1 = f2.
Proof.
(* Goal: forall (F : forall _ : R, Prop) (x f1 f2 : R) (_ : Rnd_UP_pt F x f1) (_ : Rnd_UP_pt F x f2), @eq R f1 f2 *)
intros F.
(* Goal: forall (x f1 f2 : R) (_ : Rnd_UP_pt F x f1) (_ : Rnd_UP_pt F x f2), @eq R f1 f2 *)
apply round_unicity.
(* Goal: round_pred_monotone (Rnd_UP_pt F) *)
apply Rnd_UP_pt_monotone.
Qed.

Theorem Rnd_UP_unicity :
  forall F : R -> Prop,
  forall rnd1 rnd2 : R -> R,
  Rnd_UP F rnd1 -> Rnd_UP F rnd2 ->
  forall x, rnd1 x = rnd2 x.
Proof.
(* Goal: forall (F : forall _ : R, Prop) (rnd1 rnd2 : forall _ : R, R) (_ : Rnd_UP F rnd1) (_ : Rnd_UP F rnd2) (x : R), @eq R (rnd1 x) (rnd2 x) *)
intros F rnd1 rnd2 H1 H2 x.
(* Goal: @eq R (rnd1 x) (rnd2 x) *)
now eapply Rnd_UP_pt_unicity.
Qed.

Theorem Rnd_DN_UP_pt_sym :
  forall F : R -> Prop,
  ( forall x, F x -> F (- x) ) ->
  forall x f : R,
  Rnd_DN_pt F x f -> Rnd_UP_pt F (-x) (-f).
Proof.
(* Goal: forall (F : forall _ : R, Prop) (_ : forall (x : R) (_ : F x), F (Ropp x)) (x f : R) (_ : Rnd_UP_pt F x f), Rnd_DN_pt F (Ropp x) (Ropp f) *)
intros F HF x f H.
(* Goal: Rnd_N_pt F x x *)
repeat split.
(* Goal: F (IZR Z0) *)
(* Goal: Rle x (IZR Z0) *)
apply HF.
(* Goal: Rle f (Ropp g) *)
apply H.
(* Goal: Rle (Ropp x) (Ropp d) *)
(* Goal: Rle d (IZR Z0) *)
(* Goal: round_pred_total (Rnd_NA_pt F) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
apply Ropp_le_contravar.
(* Goal: Rle f (Ropp g) *)
apply H.
(* Goal: forall (g : R) (_ : F g), Rle (Rabs (Rminus d x)) (Rabs (Rminus g x)) *)
(* Goal: or (P x d) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 d) *)
intros g Hg.
(* Goal: forall _ : Rle g (Ropp x), Rle g (Ropp f) *)
rewrite <- (Ropp_involutive g).
(* Goal: forall _ : Rle (Ropp (Ropp g)) (Ropp x), Rle (Ropp (Ropp g)) (Ropp f) *)
intros Hxg.
(* Goal: Rle (Ropp x) (Ropp d) *)
(* Goal: Rle d (IZR Z0) *)
(* Goal: round_pred_total (Rnd_NA_pt F) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
apply Ropp_le_contravar.
(* Goal: Rle f (Ropp g) *)
apply H.
(* Goal: F (IZR Z0) *)
(* Goal: Rle x (IZR Z0) *)
now apply HF.
(* Goal: Rle f x *)
now apply Ropp_le_cancel.
Qed.

Theorem Rnd_UP_DN_pt_sym :
  forall F : R -> Prop,
  ( forall x, F x -> F (- x) ) ->
  forall x f : R,
  Rnd_UP_pt F x f -> Rnd_DN_pt F (-x) (-f).
Proof.
(* Goal: forall (F : forall _ : R, Prop) (_ : forall (x : R) (_ : F x), F (Ropp x)) (x f : R) (_ : Rnd_UP_pt F x f), Rnd_DN_pt F (Ropp x) (Ropp f) *)
intros F HF x f H.
(* Goal: Rnd_N_pt F x x *)
repeat split.
(* Goal: F (IZR Z0) *)
(* Goal: Rle x (IZR Z0) *)
apply HF.
(* Goal: Rle f (Ropp g) *)
apply H.
(* Goal: Rle (Ropp x) (Ropp d) *)
(* Goal: Rle d (IZR Z0) *)
(* Goal: round_pred_total (Rnd_NA_pt F) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
apply Ropp_le_contravar.
(* Goal: Rle f (Ropp g) *)
apply H.
(* Goal: forall (g : R) (_ : F g), Rle (Rabs (Rminus d x)) (Rabs (Rminus g x)) *)
(* Goal: or (P x d) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 d) *)
intros g Hg.
(* Goal: forall _ : Rle g (Ropp x), Rle g (Ropp f) *)
rewrite <- (Ropp_involutive g).
(* Goal: forall _ : Rle (Ropp (Ropp g)) (Ropp x), Rle (Ropp (Ropp g)) (Ropp f) *)
intros Hxg.
(* Goal: Rle (Ropp x) (Ropp d) *)
(* Goal: Rle d (IZR Z0) *)
(* Goal: round_pred_total (Rnd_NA_pt F) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
apply Ropp_le_contravar.
(* Goal: Rle f (Ropp g) *)
apply H.
(* Goal: F (IZR Z0) *)
(* Goal: Rle x (IZR Z0) *)
now apply HF.
(* Goal: Rle f x *)
now apply Ropp_le_cancel.
Qed.

Theorem Rnd_DN_UP_sym :
  forall F : R -> Prop,
  ( forall x, F x -> F (- x) ) ->
  forall rnd1 rnd2 : R -> R,
  Rnd_DN F rnd1 -> Rnd_UP F rnd2 ->
  forall x, rnd1 (- x) = - rnd2 x.
Proof.
(* Goal: forall (F : forall _ : R, Prop) (_ : F (IZR Z0)) (rnd1 rnd2 : forall _ : R, R) (_ : Rnd_NA F rnd1) (_ : Rnd_NA F rnd2) (x : R), @eq R (rnd1 x) (rnd2 x) *)
intros F HF rnd1 rnd2 H1 H2 x.
(* Goal: @eq R (rnd1 (Ropp x)) (Ropp (rnd2 x)) *)
rewrite <- (Ropp_involutive (rnd1 (-x))).
(* Goal: @eq R (Rabs f) (Rabs x) *)
apply f_equal.
(* Goal: @eq R (Ropp (rnd1 (Ropp x))) (rnd2 x) *)
apply (Rnd_UP_unicity F (fun x => - rnd1 (-x))) ; trivial.
(* Goal: Rnd_UP F (fun x : R => Ropp (rnd1 (Ropp x))) *)
intros y.
(* Goal: Rnd_UP_pt F y (Ropp (rnd1 (Ropp y))) *)
pattern y at 1 ; rewrite <- Ropp_involutive.
(* Goal: Rnd_UP_pt F (Ropp (Ropp x)) (Ropp f) *)
(* Goal: round_pred_monotone (Rnd_UP_pt F) *)
apply Rnd_DN_UP_pt_sym.
(* Goal: F (IZR Z0) *)
(* Goal: Rle x (IZR Z0) *)
apply HF.
(* Goal: F f *)
(* Goal: Rle f x *)
(* Goal: Rle f f2 *)
(* Goal: Rle (Rabs f2) (Rabs f) *)
apply H1.
Qed.

Theorem Rnd_DN_UP_pt_split :
  forall F : R -> Prop,
  forall x d u,
  Rnd_DN_pt F x d ->
  Rnd_UP_pt F x u ->
  forall f, F f ->
  (f <= d) \/ (u <= f).
Proof.
(* Goal: forall (F : forall _ : R, Prop) (x d u : R) (_ : Rnd_DN_pt F x d) (_ : Rnd_UP_pt F x u) (f : R) (_ : F f), or (Rle f d) (Rle u f) *)
intros F x d u Hd Hu f Hf.
(* Goal: or (Rle f d) (Rle u f) *)
destruct (Rle_or_lt f x).
(* Goal: or (Rle (Rabs x) (Rabs u)) (Rle (Rabs x) (Rabs d)) *)
(* Goal: or (Rle (Rabs x) (Rabs u)) (Rle (Rabs x) (Rabs d)) *)
(* Goal: round_pred_total (Rnd_NA_pt F) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
left.
(* Goal: Rle g d *)
(* Goal: Rle (Rminus g x) (IZR Z0) *)
(* Goal: Rle (Rminus d x) (IZR Z0) *)
(* Goal: or (P x d) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 d) *)
now apply Hd.
(* Goal: or (Rle (Rabs x) (Rabs u)) (Rle (Rabs x) (Rabs d)) *)
(* Goal: round_pred_total (Rnd_NA_pt F) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
right.
(* Goal: Rle u f *)
assert (H' := Rlt_le _ _ H).
(* Goal: Rle u g *)
(* Goal: Rle (IZR Z0) (Rminus g x) *)
(* Goal: Rle (IZR Z0) (Rminus u x) *)
(* Goal: Rle (Rabs (Rminus d x)) (Rabs (Rminus g x)) *)
(* Goal: or (P x d) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 d) *)
now apply Hu.
Qed.

Theorem Rnd_DN_pt_refl :
  forall F : R -> Prop,
  forall x : R, F x ->
  Rnd_DN_pt F x x.
Proof.
(* Goal: forall (F : forall _ : R, Prop) (x : R) (_ : F x), Rnd_NA_pt F x x *)
intros F x Hx.
(* Goal: Rnd_N_pt F x x *)
repeat split.
(* Goal: F x *)
(* Goal: forall (g : R) (_ : F g), Rle (Rabs (Rminus x x)) (Rabs (Rminus g x)) *)
exact Hx.
(* Goal: Rle (Rabs f) (Rabs f) *)
(* Goal: @eq R f g *)
(* Goal: Rle (Rabs g) (Rabs f) *)
apply Rle_refl.
(* Goal: forall (g : R) (_ : F g) (_ : Rle x g), Rle x g *)
now intros.
Qed.

Theorem Rnd_DN_pt_idempotent :
  forall F : R -> Prop,
  forall x f : R,
  Rnd_DN_pt F x f -> F x ->
  f = x.
Proof.
(* Goal: forall (F : forall _ : R, Prop) (x f : R) (_ : Rnd_UP_pt F x f) (_ : F x), @eq R f x *)
intros F x f (_,(Hx1,Hx2)) Hx.
(* Goal: @eq R (Rabs (Rminus f x)) (Rabs (Rminus g x)) *)
(* Goal: Rle (Rabs g) (Rabs f) *)
(* Goal: Rle (Rabs g) (Rabs f) *)
apply Rle_antisym.
(* Goal: Rle x f *)
exact Hx1.
(* Goal: Rle f g *)
apply Hx2.
(* Goal: F x *)
(* Goal: forall (g : R) (_ : F g), Rle (Rabs (Rminus x x)) (Rabs (Rminus g x)) *)
exact Hx.
(* Goal: Rle (Rabs f) (Rabs f) *)
(* Goal: @eq R f g *)
(* Goal: Rle (Rabs g) (Rabs f) *)
apply Rle_refl.
Qed.

Theorem Rnd_UP_pt_refl :
  forall F : R -> Prop,
  forall x : R, F x ->
  Rnd_UP_pt F x x.
Proof.
(* Goal: forall (F : forall _ : R, Prop) (x : R) (_ : F x), Rnd_NA_pt F x x *)
intros F x Hx.
(* Goal: Rnd_N_pt F x x *)
repeat split.
(* Goal: F x *)
(* Goal: forall (g : R) (_ : F g), Rle (Rabs (Rminus x x)) (Rabs (Rminus g x)) *)
exact Hx.
(* Goal: Rle (Rabs f) (Rabs f) *)
(* Goal: @eq R f g *)
(* Goal: Rle (Rabs g) (Rabs f) *)
apply Rle_refl.
(* Goal: forall (g : R) (_ : F g) (_ : Rle x g), Rle x g *)
now intros.
Qed.

Theorem Rnd_UP_pt_idempotent :
  forall F : R -> Prop,
  forall x f : R,
  Rnd_UP_pt F x f -> F x ->
  f = x.
Proof.
(* Goal: forall (F : forall _ : R, Prop) (x f : R) (_ : Rnd_UP_pt F x f) (_ : F x), @eq R f x *)
intros F x f (_,(Hx1,Hx2)) Hx.
(* Goal: @eq R (Rabs (Rminus f x)) (Rabs (Rminus g x)) *)
(* Goal: Rle (Rabs g) (Rabs f) *)
(* Goal: Rle (Rabs g) (Rabs f) *)
apply Rle_antisym.
(* Goal: Rle f g *)
apply Hx2.
(* Goal: F x *)
(* Goal: forall (g : R) (_ : F g), Rle (Rabs (Rminus x x)) (Rabs (Rminus g x)) *)
exact Hx.
(* Goal: Rle (Rabs f) (Rabs f) *)
(* Goal: @eq R f g *)
(* Goal: Rle (Rabs g) (Rabs f) *)
apply Rle_refl.
(* Goal: Rle x f *)
exact Hx1.
Qed.

Theorem Only_DN_or_UP :
  forall F : R -> Prop,
  forall x fd fu f : R,
  Rnd_DN_pt F x fd -> Rnd_UP_pt F x fu ->
  F f -> (fd <= f <= fu)%R ->
  f = fd \/ f = fu.
Proof.
(* Goal: forall (F : forall _ : R, Prop) (x fd fu f : R) (_ : Rnd_DN_pt F x fd) (_ : Rnd_UP_pt F x fu) (_ : F f) (_ : and (Rle fd f) (Rle f fu)), or (@eq R f fd) (@eq R f fu) *)
intros F x fd fu f Hd Hu Hf [Hdf Hfu].
(* Goal: or (@eq R f fd) (@eq R f fu) *)
destruct (Rle_or_lt x f) ; [right|left].
(* Goal: @eq R f fu *)
(* Goal: @eq R f fd *)
apply Rle_antisym with (1 := Hfu).
(* Goal: Rle u g *)
(* Goal: Rle (IZR Z0) (Rminus g x) *)
(* Goal: Rle (IZR Z0) (Rminus u x) *)
(* Goal: Rle (Rabs (Rminus d x)) (Rabs (Rminus g x)) *)
(* Goal: or (P x d) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 d) *)
now apply Hu.
(* Goal: @eq R f fd *)
apply Rlt_le in H.
(* Goal: @eq R f fd *)
apply Rle_antisym with (2 := Hdf).
(* Goal: Rle g d *)
(* Goal: Rle (Rminus g x) (IZR Z0) *)
(* Goal: Rle (Rminus d x) (IZR Z0) *)
(* Goal: or (P x d) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 d) *)
now apply Hd.
Qed.

Theorem Rnd_ZR_abs :
  forall (F : R -> Prop) (rnd: R-> R),
  Rnd_ZR F rnd ->
  forall x : R,  (Rabs (rnd x) <= Rabs x)%R.
Proof.
(* Goal: forall (F : forall _ : R, Prop) (rnd : forall _ : R, R) (_ : Rnd_ZR F rnd) (x : R), Rle (Rabs (rnd x)) (Rabs x) *)
intros F rnd H x.
(* Goal: Rle (Rabs (rnd x)) (Rabs x) *)
assert (F 0%R).
(* Goal: F (IZR Z0) *)
(* Goal: Rle (Rabs (rnd x)) (Rabs x) *)
replace 0%R with (rnd 0%R).
(* Goal: Rle f (Ropp g) *)
eapply H.
(* Goal: Rle (Rabs f) (Rabs f) *)
(* Goal: @eq R f g *)
(* Goal: Rle (Rabs g) (Rabs f) *)
apply Rle_refl.
(* Goal: @eq R (rnd (IZR Z0)) (IZR Z0) *)
(* Goal: Rle (Rabs (rnd x)) (Rabs x) *)
destruct (H 0%R) as (H1, H2).
(* Goal: @eq R (Rabs (Rminus f x)) (Rabs (Rminus g x)) *)
(* Goal: Rle (Rabs g) (Rabs f) *)
(* Goal: Rle (Rabs g) (Rabs f) *)
apply Rle_antisym.
(* Goal: F f *)
(* Goal: Rle f x *)
(* Goal: Rle f f2 *)
(* Goal: Rle (Rabs f2) (Rabs f) *)
apply H1.
(* Goal: Rle (Rabs f) (Rabs f) *)
(* Goal: @eq R f g *)
(* Goal: Rle (Rabs g) (Rabs f) *)
apply Rle_refl.
(* Goal: Rle f x *)
(* Goal: Rle f f2 *)
(* Goal: Rle (Rabs f2) (Rabs f) *)
apply H2.
(* Goal: Rle (Rabs f) (Rabs f) *)
(* Goal: @eq R f g *)
(* Goal: Rle (Rabs g) (Rabs f) *)
apply Rle_refl.
(* . *)
(* Goal: Rle (Rabs (rnd x)) (Rabs x) *)
destruct (Rle_or_lt 0 x).
(* positive *)
(* Goal: or (Rle (Rabs x) (Rabs u)) (Rle (Rabs x) (Rabs d)) *)
(* Goal: round_pred_total (Rnd_NA_pt F) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
rewrite Rabs_right.
(* Goal: Rle (rnd x) (Rabs x) *)
(* Goal: Rge (rnd x) (IZR Z0) *)
(* Goal: Rle (Rabs (rnd x)) (Rabs x) *)
rewrite Rabs_right; auto with real.
(* Goal: Rle (IZR Z0) (rnd x) *)
(* Goal: Rle (Rabs (rnd x)) (Rabs x) *)
now apply (proj1 (H x)).
(* Goal: Rge (rnd x) (IZR Z0) *)
(* Goal: Rle (Rabs (rnd x)) (Rabs x) *)
apply Rle_ge.
(* Goal: Rle (IZR Z0) (rnd x) *)
(* Goal: Rle (Rabs (rnd x)) (Rabs x) *)
now apply (proj1 (H x)).
(* negative *)
(* Goal: Rle (Ropp x) (Rabs d) *)
(* Goal: round_pred_total (Rnd_NA_pt F) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
rewrite Rabs_left1.
(* Goal: Rle (Ropp (rnd x)) (Rabs x) *)
(* Goal: Rle (rnd x) (IZR Z0) *)
rewrite Rabs_left1 ; auto with real.
(* Goal: Rle (Ropp x) (Ropp d) *)
(* Goal: Rle d (IZR Z0) *)
(* Goal: round_pred_total (Rnd_NA_pt F) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
apply Ropp_le_contravar.
(* Goal: Rle x (rnd x) *)
(* Goal: Rle (rnd x) (IZR Z0) *)
apply (proj2 (H x)).
(* Goal: Rle x (IZR Z0) *)
(* Goal: Rle (rnd x) (IZR Z0) *)
auto with real.
(* Goal: Rle x (IZR Z0) *)
(* Goal: Rle (rnd x) (IZR Z0) *)
apply (proj2 (H x)) ; auto with real.
Qed.

Theorem Rnd_ZR_pt_monotone :
  forall F : R -> Prop, F 0 ->
  round_pred_monotone (Rnd_ZR_pt F).
Proof.
(* Goal: forall (F : forall _ : R, Prop) (_ : F (IZR Z0)), round_pred_monotone (Rnd_ZR_pt F) *)
intros F F0 x y f g (Hx1, Hx2) (Hy1, Hy2) Hxy.
(* Goal: @ex R (fun f : R => Rnd_ZR_pt F x f) *)
(* Goal: round_pred_monotone (Rnd_ZR_pt F) *)
destruct (Rle_or_lt 0 x) as [Hx|Hx].
(* . *)
(* Goal: Rle f g *)
(* Goal: Rle f g *)
apply Hy1.
(* Goal: Rle (IZR Z0) y *)
(* Goal: F f *)
(* Goal: Rle f y *)
(* Goal: Rle f g *)
now apply Rle_trans with x.
(* Goal: F f *)
(* Goal: Rle f y *)
now apply Hx1.
(* Goal: Rle f y *)
(* Goal: Rle f g *)
apply Rle_trans with (2 := Hxy).
(* Goal: F f *)
(* Goal: Rle f y *)
now apply Hx1.
(* . *)
(* Goal: Rle d (IZR Z0) *)
(* Goal: round_pred_total (Rnd_NA_pt F) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
apply Rlt_le in Hx.
(* Goal: Rle f g *)
destruct (Rle_or_lt 0 y) as [Hy|Hy].
(* Goal: Rle f g *)
(* Goal: Rle f g *)
apply Rle_trans with 0.
(* Goal: Rle f g *)
now apply Hx2.
(* Goal: Rle f g *)
(* Goal: Rle f g *)
now apply Hy1.
(* Goal: Rle f g *)
apply Rlt_le in Hy.
(* Goal: Rle f g *)
apply Hx2.
(* Goal: F x *)
(* Goal: forall (g : R) (_ : F g), Rle (Rabs (Rminus x x)) (Rabs (Rminus g x)) *)
exact Hx.
(* Goal: Rle f g *)
now apply Hy2.
(* Goal: Rle x g *)
apply Rle_trans with (1 := Hxy).
(* Goal: Rle f g *)
now apply Hy2.
Qed.

Theorem Rnd_N_pt_DN_or_UP :
  forall F : R -> Prop,
  forall x f : R,
  Rnd_N_pt F x f ->
  Rnd_DN_pt F x f \/ Rnd_UP_pt F x f.
Proof.
(* Goal: forall (F : forall _ : R, Prop) (x f : R) (_ : Rnd_N_pt F x f), or (Rnd_DN_pt F x f) (Rnd_UP_pt F x f) *)
intros F x f (Hf1,Hf2).
(* Goal: or (Rnd_DN_pt F x f) (Rnd_UP_pt F x f) *)
destruct (Rle_or_lt x f) as [Hxf|Hxf].
(* . *)
(* Goal: or (Rle (Rabs x) (Rabs u)) (Rle (Rabs x) (Rabs d)) *)
(* Goal: round_pred_total (Rnd_NA_pt F) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
right.
(* Goal: Rnd_DN_pt F x f *)
repeat split ; try assumption.
(* Goal: forall (g : R) (_ : F g) (_ : Rle g x), Rle g f *)
intros g Hg Hxg.
(* Goal: Rle g f *)
specialize (Hf2 g Hg).
(* Goal: Rle f g *)
(* Goal: or (Rnd_DN_pt F x f) (Rnd_UP_pt F x f) *)
rewrite 2!Rabs_pos_eq in Hf2.
(* Goal: Rle g f *)
(* Goal: Rle (Rminus g x) (IZR Z0) *)
(* Goal: Rle (Rminus f x) (IZR Z0) *)
now apply Rplus_le_reg_r with (-x)%R.
(* Goal: Rle (IZR Z0) (Rminus g x) *)
(* Goal: Rle (IZR Z0) (Rminus u x) *)
(* Goal: Rle (Rabs (Rminus d x)) (Rabs (Rminus g x)) *)
(* Goal: or (P x d) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 d) *)
now apply Rle_0_minus.
(* Goal: Rle (IZR Z0) (Rminus g x) *)
(* Goal: Rle (IZR Z0) (Rminus u x) *)
(* Goal: Rle (Rabs (Rminus d x)) (Rabs (Rminus g x)) *)
(* Goal: or (P x d) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 d) *)
now apply Rle_0_minus.
(* . *)
(* Goal: or (Rle (Rabs x) (Rabs u)) (Rle (Rabs x) (Rabs d)) *)
(* Goal: or (Rle (Rabs x) (Rabs u)) (Rle (Rabs x) (Rabs d)) *)
(* Goal: round_pred_total (Rnd_NA_pt F) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
left.
(* Goal: Rnd_DN_pt F x f *)
repeat split ; try assumption.
(* Goal: Rle x (IZR Z0) *)
now apply Rlt_le.
(* Goal: forall (g : R) (_ : F g) (_ : Rle g x), Rle g f *)
intros g Hg Hxg.
(* Goal: Rle g f *)
specialize (Hf2 g Hg).
(* Goal: Rle g f *)
rewrite 2!Rabs_left1 in Hf2.
(* Goal: Rle g f *)
(* Goal: Rle (Rminus g x) (IZR Z0) *)
(* Goal: Rle (Rminus f x) (IZR Z0) *)
generalize (Ropp_le_cancel _ _ Hf2).
(* Goal: forall _ : Rle (Rminus g x) (Rminus f x), Rle g f *)
(* Goal: Rle (Rminus g x) (IZR Z0) *)
(* Goal: Rle (Rminus f x) (IZR Z0) *)
intros H.
(* Goal: Rle g f *)
(* Goal: Rle (Rminus g x) (IZR Z0) *)
(* Goal: Rle (Rminus f x) (IZR Z0) *)
now apply Rplus_le_reg_r with (-x)%R.
(* Goal: Rle (Rminus g x) (IZR Z0) *)
(* Goal: Rle (Rminus d x) (IZR Z0) *)
(* Goal: or (P x d) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 d) *)
now apply Rle_minus.
(* Goal: Rle (Rabs (Rminus d x)) (Rabs (Rminus g x)) *)
(* Goal: Rle (Rabs (Rminus d x)) (Rabs (Rminus g x)) *)
(* Goal: or (P x d) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 d) *)
apply Rlt_le.
(* Goal: Rlt (Rminus f x) (IZR Z0) *)
now apply Rlt_minus.
Qed.

Theorem Rnd_N_pt_DN_or_UP_eq :
  forall F : R -> Prop,
  forall x fd fu f : R,
  Rnd_DN_pt F x fd -> Rnd_UP_pt F x fu ->
  Rnd_N_pt F x f ->
  f = fd \/ f = fu.
Proof.
(* Goal: forall (F : forall _ : R, Prop) (x fd fu f : R) (_ : Rnd_DN_pt F x fd) (_ : Rnd_UP_pt F x fu) (_ : Rnd_N_pt F x f), or (@eq R f fd) (@eq R f fu) *)
intros F x fd fu f Hd Hu Hf.
(* Goal: or (@eq R f fd) (@eq R f fu) *)
destruct (Rnd_N_pt_DN_or_UP F x f Hf) as [H|H].
(* Goal: or (Rle (Rabs x) (Rabs u)) (Rle (Rabs x) (Rabs d)) *)
(* Goal: or (Rle (Rabs x) (Rabs u)) (Rle (Rabs x) (Rabs d)) *)
(* Goal: round_pred_total (Rnd_NA_pt F) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
left.
(* Goal: @eq R f fd *)
(* Goal: or (@eq R f fd) (@eq R f fu) *)
apply Rnd_DN_pt_unicity with (1 := H) (2 := Hd).
(* Goal: or (Rle (Rabs x) (Rabs u)) (Rle (Rabs x) (Rabs d)) *)
(* Goal: round_pred_total (Rnd_NA_pt F) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
right.
(* Goal: @eq R f fu *)
apply Rnd_UP_pt_unicity with (1 := H) (2 := Hu).
Qed.

Theorem Rnd_N_pt_sym :
  forall F : R -> Prop,
  ( forall x, F x -> F (- x) ) ->
  forall x f : R,
  Rnd_N_pt F (-x) (-f) -> Rnd_N_pt F x f.
Proof.
(* Goal: forall (F : forall _ : R, Prop) (_ : forall (x : R) (_ : F x), F (Ropp x)) (x f : R) (_ : Rnd_N_pt F (Ropp x) (Ropp f)), Rnd_N_pt F x f *)
intros F HF x f (H1,H2).
(* Goal: @eq R f2 f *)
rewrite <- (Ropp_involutive f).
(* Goal: Rnd_N_pt F x x *)
repeat split.
(* Goal: F (IZR Z0) *)
(* Goal: Rle x (IZR Z0) *)
apply HF.
(* Goal: F f *)
(* Goal: Rle f x *)
(* Goal: Rle f f2 *)
(* Goal: Rle (Rabs f2) (Rabs f) *)
apply H1.
(* Goal: forall (g : R) (_ : F g), Rle (Rabs (Rminus (Ropp (Ropp f)) x)) (Rabs (Rminus g x)) *)
intros g H3.
(* Goal: Rle (Rabs (Rminus (Ropp (Ropp f)) x)) (Rabs (Rminus g x)) *)
rewrite Ropp_involutive.
(* Goal: Rle (Rabs (Rminus f x)) (Rabs (Rminus g x)) *)
replace (f - x)%R with (-(-f - -x))%R by ring.
(* Goal: Rle (Rabs (Ropp (Rminus (Ropp f) (Ropp x)))) (Rabs (Rminus g x)) *)
replace (g - x)%R with (-(-g - -x))%R by ring.
(* Goal: Rle (Rabs (Ropp (Rminus (Ropp f) (Ropp x)))) (Rabs (Ropp (Rminus (Ropp g) (Ropp x)))) *)
rewrite 2!Rabs_Ropp.
(* Goal: Rle f x *)
(* Goal: Rle f f2 *)
(* Goal: Rle (Rabs f2) (Rabs f) *)
apply H2.
(* Goal: F (IZR Z0) *)
(* Goal: Rle x (IZR Z0) *)
now apply HF.
Qed.

Theorem Rnd_N_pt_monotone :
  forall F : R -> Prop,
  forall x y f g : R,
  Rnd_N_pt F x f -> Rnd_N_pt F y g ->
  x < y -> f <= g.
Proof.
intros F x y f g (Hf,Hx) (Hg,Hy) Hxy.
apply Rnot_lt_le.
intros Hgf.
assert (Hfgx := Hx g Hg).
assert (Hgfy := Hy f Hf).
clear F Hf Hg Hx Hy.
destruct (Rle_or_lt x g) as [Hxg|Hgx].
(* x <= g < f *)
apply Rle_not_lt with (1 := Hfgx).
(* Goal: Rle (Rabs (Rminus u x)) (Rabs (Rminus g x)) *)
(* Goal: Rle (Rabs (Rminus d x)) (Rabs (Rminus g x)) *)
(* Goal: or (P x d) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 d) *)
rewrite 2!Rabs_pos_eq.
now apply Rplus_lt_compat_r.
(* Goal: Rle (IZR Z0) (Rminus u x) *)
(* Goal: Rle (Rabs (Rminus d x)) (Rabs (Rminus g x)) *)
(* Goal: or (P x d) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 d) *)
apply Rle_0_minus.
(* Goal: Rle (Rabs (Rminus d x)) (Rabs (Rminus g x)) *)
(* Goal: Rle (Rabs (Rminus d x)) (Rabs (Rminus g x)) *)
(* Goal: or (P x d) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 d) *)
apply Rlt_le.
now apply Rle_lt_trans with (1 := Hxg).
(* Goal: Rle (IZR Z0) (Rminus g x) *)
(* Goal: Rle (IZR Z0) (Rminus u x) *)
(* Goal: Rle (Rabs (Rminus d x)) (Rabs (Rminus g x)) *)
(* Goal: or (P x d) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 d) *)
now apply Rle_0_minus.
assert (Hgy := Rlt_trans _ _ _ Hgx Hxy).
destruct (Rle_or_lt f y) as [Hfy|Hyf].
(* g < f <= y *)
apply Rle_not_lt with (1 := Hgfy).
rewrite (Rabs_left (g - y)).
(* Goal: Rlt (Rminus f x) (IZR Z0) *)
2: now apply Rlt_minus.
(* Goal: Rle (Ropp x) (Rabs d) *)
(* Goal: round_pred_total (Rnd_NA_pt F) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
rewrite Rabs_left1.
apply Ropp_lt_contravar.
now apply Rplus_lt_compat_r.
(* Goal: Rle (Rminus g x) (IZR Z0) *)
(* Goal: Rle (Rminus d x) (IZR Z0) *)
(* Goal: or (P x d) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 d) *)
now apply Rle_minus.
(* g < x < y < f *)
rewrite Rabs_left, Rabs_pos_eq, Ropp_minus_distr in Hgfy.
rewrite Rabs_pos_eq, Rabs_left, Ropp_minus_distr in Hfgx.
apply Rle_not_lt with (1 := Rplus_le_compat _ _ _ _ Hfgx Hgfy).
apply Rminus_lt.
(* Goal: Rle (Rplus f f) (Rplus (Rminus (Rmult (IZR (Zpos (xO xH))) x) f) f) *)
ring_simplify.
apply Rlt_minus.
apply Rmult_lt_compat_l.
now apply (Z2R_lt 0 2).
(* Goal: Rle x y *)
exact Hxy.
(* Goal: Rlt (Rminus f x) (IZR Z0) *)
now apply Rlt_minus.
(* Goal: Rle (IZR Z0) (Rminus u x) *)
(* Goal: Rle (Rabs (Rminus d x)) (Rabs (Rminus g x)) *)
(* Goal: or (P x d) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 d) *)
apply Rle_0_minus.
(* Goal: Rle (Rabs (Rminus d x)) (Rabs (Rminus g x)) *)
(* Goal: Rle (Rabs (Rminus d x)) (Rabs (Rminus g x)) *)
(* Goal: or (P x d) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 d) *)
apply Rlt_le.
now apply Rlt_trans with (1 := Hxy).
(* Goal: Rle (IZR Z0) (Rminus u x) *)
(* Goal: Rle (Rabs (Rminus d x)) (Rabs (Rminus g x)) *)
(* Goal: or (P x d) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 d) *)
apply Rle_0_minus.
(* Goal: Rle x (IZR Z0) *)
now apply Rlt_le.
(* Goal: Rlt (Rminus f x) (IZR Z0) *)
now apply Rlt_minus.
Qed.

Theorem Rnd_N_pt_unicity :
  forall F : R -> Prop,
  forall x d u f1 f2 : R,
  Rnd_DN_pt F x d ->
  Rnd_UP_pt F x u ->
  x - d <> u - x ->
  Rnd_N_pt F x f1 ->
  Rnd_N_pt F x f2 ->
  f1 = f2.
Proof.
(* Goal: forall (F : forall _ : R, Prop) (x d u f1 f2 : R) (_ : Rnd_DN_pt F x d) (_ : Rnd_UP_pt F x u) (_ : not (@eq R (Rminus x d) (Rminus u x))) (_ : Rnd_N_pt F x f1) (_ : Rnd_N_pt F x f2), @eq R f1 f2 *)
intros F x d u f1 f2 Hd Hu Hdu.
(* Goal: forall (_ : Rnd_N_pt F x f1) (_ : Rnd_N_pt F x f2), @eq R f1 f2 *)
assert (forall f1 f2, Rnd_N_pt F x f1 -> Rnd_N_pt F x f2 -> f1 < f2 -> False).
(* Goal: forall (f1 f2 : R) (_ : Rnd_N_pt F x f1) (_ : Rnd_N_pt F x f2) (_ : Rlt f1 f2), False *)
(* Goal: forall (_ : Rnd_N_pt F x f1) (_ : Rnd_N_pt F x f2), @eq R f1 f2 *)
clear f1 f2. intros f1 f2 Hf1 Hf2 H12.
destruct (Rnd_N_pt_DN_or_UP F x f1 Hf1) as [Hd1|Hu1] ;
  destruct (Rnd_N_pt_DN_or_UP F x f2 Hf2) as [Hd2|Hu2].
(* Goal: False *)
(* Goal: False *)
(* Goal: False *)
(* Goal: False *)
(* Goal: forall (_ : Rnd_N_pt F x f1) (_ : Rnd_N_pt F x f2), @eq R f1 f2 *)
apply Rlt_not_eq with (1 := H12).
(* Goal: @eq R f1 f2 *)
(* Goal: False *)
(* Goal: False *)
(* Goal: False *)
(* Goal: forall (_ : Rnd_N_pt F x f1) (_ : Rnd_N_pt F x f2), @eq R f1 f2 *)
now apply Rnd_DN_pt_unicity with (1 := Hd1).
(* Goal: False *)
(* Goal: False *)
(* Goal: False *)
(* Goal: forall (_ : Rnd_N_pt F x f1) (_ : Rnd_N_pt F x f2), @eq R f1 f2 *)
apply Hdu.
(* Goal: @eq R (Rminus x d) (Rminus u x) *)
(* Goal: False *)
(* Goal: False *)
(* Goal: forall (_ : Rnd_N_pt F x f1) (_ : Rnd_N_pt F x f2), @eq R f1 f2 *)
rewrite Rnd_DN_pt_unicity with (1 := Hd) (2 := Hd1).
(* Goal: @eq R (Rminus x f1) (Rminus u x) *)
(* Goal: False *)
(* Goal: False *)
(* Goal: forall (_ : Rnd_N_pt F x f1) (_ : Rnd_N_pt F x f2), @eq R f1 f2 *)
rewrite Rnd_UP_pt_unicity with (1 := Hu) (2 := Hu2).
(* Goal: @eq R (Rminus x f1) (Rminus f2 x) *)
(* Goal: False *)
(* Goal: False *)
(* Goal: forall (_ : Rnd_N_pt F x f1) (_ : Rnd_N_pt F x f2), @eq R f1 f2 *)
rewrite <- (Rabs_pos_eq (x - f1)).
(* Goal: @eq R (Rabs (Rminus x f1)) (Rminus f2 x) *)
(* Goal: Rle (IZR Z0) (Rminus x f1) *)
(* Goal: False *)
(* Goal: False *)
(* Goal: forall (_ : Rnd_N_pt F x f1) (_ : Rnd_N_pt F x f2), @eq R f1 f2 *)
rewrite <- (Rabs_pos_eq (f2 - x)).
(* Goal: @eq R (Rabs (Rminus d x)) (Rminus x d) *)
(* Goal: Rnd_N_pt F x d *)
rewrite Rabs_minus_sym.
(* Goal: @eq R (Rabs (Rminus f x)) (Rabs (Rminus g x)) *)
(* Goal: Rle (Rabs g) (Rabs f) *)
(* Goal: Rle (Rabs g) (Rabs f) *)
apply Rle_antisym.
(* Goal: F f1 *)
(* Goal: Rle (IZR Z0) (Rminus f2 x) *)
(* Goal: Rle (IZR Z0) (Rminus x f1) *)
(* Goal: False *)
(* Goal: False *)
(* Goal: forall (_ : Rnd_N_pt F x f1) (_ : Rnd_N_pt F x f2), @eq R f1 f2 *)
apply Hf1. apply Hf2.
(* Goal: F f1 *)
(* Goal: Rle (IZR Z0) (Rminus f2 x) *)
(* Goal: Rle (IZR Z0) (Rminus x f1) *)
(* Goal: False *)
(* Goal: False *)
(* Goal: forall (_ : Rnd_N_pt F x f1) (_ : Rnd_N_pt F x f2), @eq R f1 f2 *)
apply Hf2. apply Hf1.
(* Goal: Rle (IZR Z0) (Rminus u x) *)
(* Goal: Rle (Rabs (Rminus d x)) (Rabs (Rminus g x)) *)
(* Goal: or (P x d) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 d) *)
apply Rle_0_minus.
(* Goal: Rle x f2 *)
(* Goal: Rle (IZR Z0) (Rminus x f1) *)
(* Goal: False *)
(* Goal: False *)
(* Goal: forall (_ : Rnd_N_pt F x f1) (_ : Rnd_N_pt F x f2), @eq R f1 f2 *)
apply Hu2.
(* Goal: Rle (IZR Z0) (Rminus u x) *)
(* Goal: Rle (Rabs (Rminus d x)) (Rabs (Rminus g x)) *)
(* Goal: or (P x d) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 d) *)
apply Rle_0_minus.
(* Goal: Rle f1 x *)
(* Goal: False *)
(* Goal: False *)
(* Goal: forall (_ : Rnd_N_pt F x f1) (_ : Rnd_N_pt F x f2), @eq R f1 f2 *)
apply Hd1.
(* Goal: False *)
(* Goal: False *)
(* Goal: forall (_ : Rnd_N_pt F x f1) (_ : Rnd_N_pt F x f2), @eq R f1 f2 *)
apply Rlt_not_le with (1 := H12).
(* Goal: Rle d u *)
(* Goal: Rle u d *)
apply Rle_trans with x.
(* Goal: Rle f2 x *)
(* Goal: Rle x f1 *)
(* Goal: False *)
(* Goal: forall (_ : Rnd_N_pt F x f1) (_ : Rnd_N_pt F x f2), @eq R f1 f2 *)
apply Hd2.
(* Goal: Rle x f1 *)
(* Goal: False *)
(* Goal: forall (_ : Rnd_N_pt F x f1) (_ : Rnd_N_pt F x f2), @eq R f1 f2 *)
apply Hu1.
(* Goal: False *)
(* Goal: forall (_ : Rnd_N_pt F x f1) (_ : Rnd_N_pt F x f2), @eq R f1 f2 *)
apply Rgt_not_eq with (1 := H12).
(* Goal: @eq R f2 f1 *)
(* Goal: forall (_ : Rnd_N_pt F x f1) (_ : Rnd_N_pt F x f2), @eq R f1 f2 *)
now apply Rnd_UP_pt_unicity with (1 := Hu2).
(* Goal: forall (_ : Rnd_N_pt F x f1) (_ : Rnd_N_pt F x f2), @eq R f1 f2 *)
intros Hf1 Hf2.
(* Goal: @eq R f1 f2 *)
now apply Rle_antisym ; apply Rnot_lt_le ; refine (H _ _ _ _).
Qed.

Theorem Rnd_N_pt_refl :
  forall F : R -> Prop,
  forall x : R, F x ->
  Rnd_N_pt F x x.
Proof.
(* Goal: forall (F : forall _ : R, Prop) (x : R) (_ : F x), Rnd_NA_pt F x x *)
intros F x Hx.
(* Goal: Rnd_N_pt F x x *)
repeat split.
(* Goal: F x *)
(* Goal: forall (g : R) (_ : F g), Rle (Rabs (Rminus x x)) (Rabs (Rminus g x)) *)
exact Hx.
(* Goal: forall (g : R) (_ : F g), Rle (Rabs (Rminus (IZR Z0) (IZR Z0))) (Rabs (Rminus g (IZR Z0))) *)
intros g _.
(* Goal: Rle (Rabs (Rminus x x)) (Rabs (Rminus g x)) *)
unfold Rminus at 1.
(* Goal: Rle (Rabs (Rplus x (Ropp x))) (Rabs (Rminus g x)) *)
rewrite Rplus_opp_r, Rabs_R0.
(* Goal: Rle (IZR Z0) (Rabs g) *)
apply Rabs_pos.
Qed.

Theorem Rnd_N_pt_idempotent :
  forall F : R -> Prop,
  forall x f : R,
  Rnd_N_pt F x f -> F x ->
  f = x.
Proof.
(* Goal: forall (F : forall _ : R, Prop) (x f : R) (_ : Rnd_N_pt F x f) (_ : F x), @eq R f x *)
intros F x f (_,Hf) Hx.
(* Goal: @eq R f x *)
apply Rminus_diag_uniq.
(* Goal: @eq R (Rminus f x) (IZR Z0) *)
destruct (Req_dec (f - x) 0) as [H|H].
(* Goal: Rle k b *)
(* Goal: Rle x k *)
(* Goal: Rle f k *)
exact H.
(* Goal: @eq R (Rminus f x) (IZR Z0) *)
elim Rabs_no_R0 with (1 := H).
(* Goal: @eq R (Rabs (Rminus f x)) (Rabs (Rminus g x)) *)
(* Goal: Rle (Rabs g) (Rabs f) *)
(* Goal: Rle (Rabs g) (Rabs f) *)
apply Rle_antisym.
(* Goal: Rle (Rabs (Rminus f x)) (IZR Z0) *)
(* Goal: Rle (IZR Z0) (Rabs (Rminus f x)) *)
replace 0 with (Rabs (x - x)).
(* Goal: Rle (Rabs (Rminus f x)) (Rabs (Rminus x x)) *)
(* Goal: @eq R (Rabs (Rminus x x)) (IZR Z0) *)
(* Goal: Rle (IZR Z0) (Rabs (Rminus f x)) *)
now apply Hf.
(* Goal: @eq R (Rabs (Rminus x x)) (IZR Z0) *)
(* Goal: Rle (IZR Z0) (Rabs (Rminus f x)) *)
unfold Rminus.
(* Goal: @eq R (Rabs (Rplus x (Ropp x))) (IZR Z0) *)
(* Goal: Rle (IZR Z0) (Rabs (Rminus f x)) *)
rewrite Rplus_opp_r.
(* Goal: @eq R (Rabs (IZR Z0)) (IZR Z0) *)
(* Goal: Rle (IZR Z0) (Rabs (Rminus f x)) *)
apply Rabs_R0.
(* Goal: Rle (IZR Z0) (Rabs g) *)
apply Rabs_pos.
Qed.

Theorem Rnd_N_pt_0 :
  forall F : R -> Prop,
  F 0 ->
  Rnd_N_pt F 0 0.
Proof.
(* Goal: forall (F : forall _ : R, Prop) (_ : F (IZR Z0)), Rnd_N_pt F (IZR Z0) (IZR Z0) *)
intros F HF.
(* Goal: round_pred (Rnd_NA_pt F) *)
split.
(* Goal: forall (x : R) (_ : F x), F (Ropp x) *)
(* Goal: Rnd_N_pt F (Ropp (Ropp x)) (Ropp (Ropp f2)) *)
exact HF.
(* Goal: forall (g : R) (_ : F g), Rle (Rabs (Rminus (IZR Z0) (IZR Z0))) (Rabs (Rminus g (IZR Z0))) *)
intros g _.
(* Goal: Rle (Rabs (Rminus (IZR Z0) (IZR Z0))) (Rabs (Rminus g (IZR Z0))) *)
rewrite 2!Rminus_0_r, Rabs_R0.
(* Goal: Rle (IZR Z0) (Rabs g) *)
apply Rabs_pos.
Qed.

Theorem Rnd_N_pt_pos :
  forall F : R -> Prop, F 0 ->
  forall x f, 0 <= x ->
  Rnd_N_pt F x f ->
  0 <= f.
Proof.
(* Goal: forall (F : forall _ : R, Prop) (_ : F (IZR Z0)) (x f : R) (_ : Rle x (IZR Z0)) (_ : Rnd_N_pt F x f), Rle f (IZR Z0) *)
intros F HF x f [Hx|Hx] Hxf.
(* Goal: Rle f (IZR Z0) *)
(* Goal: Rle f (IZR Z0) *)
eapply Rnd_N_pt_monotone ; try eassumption.
(* Goal: Rnd_N_pt F (IZR Z0) (IZR Z0) *)
(* Goal: Rle f (IZR Z0) *)
now apply Rnd_N_pt_0.
(* Goal: or (Rle (Rabs x) (Rabs u)) (Rle (Rabs x) (Rabs d)) *)
(* Goal: round_pred_total (Rnd_NA_pt F) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
right.
(* Goal: @eq R x d *)
(* Goal: @ex R (fun f : R => Rnd_NG_pt F P x f) *)
(* Goal: @ex R (fun f : R => Rnd_NG_pt F P x f) *)
apply sym_eq.
(* Goal: @eq R f (IZR Z0) *)
apply Rnd_N_pt_idempotent with F.
(* Goal: Rnd_N_pt F (IZR Z0) f *)
(* Goal: F (IZR Z0) *)
now rewrite Hx.
(* Goal: forall (x : R) (_ : F x), F (Ropp x) *)
(* Goal: Rnd_N_pt F (Ropp (Ropp x)) (Ropp (Ropp f2)) *)
exact HF.
Qed.

Theorem Rnd_N_pt_neg :
  forall F : R -> Prop, F 0 ->
  forall x f, x <= 0 ->
  Rnd_N_pt F x f ->
  f <= 0.
Proof.
(* Goal: forall (F : forall _ : R, Prop) (_ : F (IZR Z0)) (x f : R) (_ : Rle x (IZR Z0)) (_ : Rnd_N_pt F x f), Rle f (IZR Z0) *)
intros F HF x f [Hx|Hx] Hxf.
(* Goal: Rle f (IZR Z0) *)
(* Goal: Rle f (IZR Z0) *)
eapply Rnd_N_pt_monotone ; try eassumption.
(* Goal: Rnd_N_pt F (IZR Z0) (IZR Z0) *)
(* Goal: Rle f (IZR Z0) *)
now apply Rnd_N_pt_0.
(* Goal: or (Rle (Rabs x) (Rabs u)) (Rle (Rabs x) (Rabs d)) *)
(* Goal: round_pred_total (Rnd_NA_pt F) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
right.
(* Goal: @eq R f (IZR Z0) *)
apply Rnd_N_pt_idempotent with F.
(* Goal: Rnd_N_pt F (IZR Z0) f *)
(* Goal: F (IZR Z0) *)
now rewrite <- Hx.
(* Goal: forall (x : R) (_ : F x), F (Ropp x) *)
(* Goal: Rnd_N_pt F (Ropp (Ropp x)) (Ropp (Ropp f2)) *)
exact HF.
Qed.

Theorem Rnd_N_pt_abs :
  forall F : R -> Prop,
  F 0 ->
  ( forall x, F x -> F (- x) ) ->
  forall x f : R,
  Rnd_N_pt F x f -> Rnd_N_pt F (Rabs x) (Rabs f).
Proof.
(* Goal: forall (F : forall _ : R, Prop) (_ : F (IZR Z0)) (_ : forall (x : R) (_ : F x), F (Ropp x)) (x f : R) (_ : Rnd_N_pt F x f), Rnd_N_pt F (Rabs x) (Rabs f) *)
intros F HF0 HF x f Hxf.
(* Goal: Rnd_N_pt F (Rabs x) (Rabs f) *)
unfold Rabs at 1.
(* Goal: Rnd_N_pt F (if Rcase_abs x then Ropp x else x) (Rabs f) *)
destruct (Rcase_abs x) as [Hx|Hx].
(* Goal: Rle (Ropp x) (Rabs d) *)
(* Goal: round_pred_total (Rnd_NA_pt F) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
rewrite Rabs_left1.
(* Goal: Rnd_N_pt F (Ropp x) (Ropp f2) *)
apply Rnd_N_pt_sym.
(* Goal: forall (x : R) (_ : F x), F (Ropp x) *)
(* Goal: Rnd_N_pt F (Ropp (Ropp x)) (Ropp (Ropp f2)) *)
exact HF.
(* Goal: Rnd_N_pt F (Ropp (Ropp x)) (Ropp (Ropp f2)) *)
now rewrite 2!Ropp_involutive.
(* Goal: Rle f (IZR Z0) *)
(* Goal: Rnd_N_pt F x (Rabs f) *)
apply Rnd_N_pt_neg with (3 := Hxf).
(* Goal: F (IZR Z0) *)
(* Goal: Rle (IZR Z0) x *)
exact HF0.
(* Goal: Rle x (IZR Z0) *)
now apply Rlt_le.
(* Goal: Rle x (Rabs u) *)
(* Goal: or (Rle (Rabs x) (Rabs u)) (Rle (Rabs x) (Rabs d)) *)
(* Goal: round_pred_total (Rnd_NA_pt F) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
rewrite Rabs_pos_eq.
(* Goal: Rnd_N_pt F x f *)
(* Goal: Rle (IZR Z0) f *)
exact Hxf.
(* Goal: Rle (IZR Z0) f *)
apply Rnd_N_pt_pos with (3 := Hxf).
(* Goal: F (IZR Z0) *)
(* Goal: Rle (IZR Z0) x *)
exact HF0.
(* Goal: Rle (IZR Z0) x *)
now apply Rge_le.
Qed.

Theorem Rnd_DN_UP_pt_N :
  forall F : R -> Prop,
  forall x d u f : R,
  F f ->
  Rnd_DN_pt F x d ->
  Rnd_UP_pt F x u ->
  (Rabs (f - x) <= x - d)%R ->
  (Rabs (f - x) <= u - x)%R ->
  Rnd_N_pt F x f.
Proof.
(* Goal: forall (F : forall _ : R, Prop) (x d u f : R) (_ : F f) (_ : Rnd_DN_pt F x d) (_ : Rnd_UP_pt F x u) (_ : Rle (Rabs (Rminus f x)) (Rminus x d)) (_ : Rle (Rabs (Rminus f x)) (Rminus u x)), Rnd_N_pt F x f *)
intros F x d u f Hf Hxd Hxu Hd Hu.
(* Goal: round_pred (Rnd_NA_pt F) *)
split.
(* Goal: Rnd_DN_pt F (Ropp x) f *)
(* Goal: round_pred_monotone (Rnd_UP_pt F) *)
exact Hf.
(* Goal: forall (g : R) (_ : F g), Rle (Rabs (Rminus d x)) (Rabs (Rminus g x)) *)
(* Goal: or (P x d) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 d) *)
intros g Hg.
(* Goal: Rle (Rabs (Rminus f x)) (Rabs (Rminus g x)) *)
destruct (Rnd_DN_UP_pt_split F x d u Hxd Hxu g Hg) as [Hgd|Hgu].
(* g <= d *)
(* Goal: Rle (Rabs (Rminus f x)) (Rabs (Rminus g x)) *)
(* Goal: Rle (Rabs (Rminus f x)) (Rabs (Rminus g x)) *)
apply Rle_trans with (1 := Hd).
(* Goal: Rle (Ropp x) (Rabs d) *)
(* Goal: round_pred_total (Rnd_NA_pt F) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
rewrite Rabs_left1.
(* Goal: Rle (Rminus x d) (Ropp (Rminus g x)) *)
(* Goal: Rle (Rminus g x) (IZR Z0) *)
(* Goal: Rle (Rabs (Rminus f x)) (Rabs (Rminus g x)) *)
rewrite Ropp_minus_distr.
(* Goal: Rle (Rminus x d) (Rminus x g) *)
(* Goal: Rle (IZR Z0) (Rminus x g) *)
(* Goal: Rle (IZR Z0) (Rminus x d) *)
(* Goal: or (P x u) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 u) *)
(* Goal: @ex R (fun f : R => Rnd_NG_pt F P x f) *)
(* Goal: @ex R (fun f : R => Rnd_NG_pt F P x f) *)
apply Rplus_le_compat_l.
(* Goal: Rle (Ropp x) (Ropp d) *)
(* Goal: Rle d (IZR Z0) *)
(* Goal: round_pred_total (Rnd_NA_pt F) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
now apply Ropp_le_contravar.
(* Goal: Rle (Rminus d x) (IZR Z0) *)
(* Goal: or (P x d) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 d) *)
apply Rle_minus.
(* Goal: Rle g x *)
(* Goal: Rle (Rabs (Rminus f x)) (Rabs (Rminus g x)) *)
apply Rle_trans with (1 := Hgd).
(* Goal: Rle d x *)
(* Goal: Rle (Rabs (Rminus f x)) (Rabs (Rminus g x)) *)
apply Hxd.
(* u <= g *)
(* Goal: Rle (Rabs (Rminus f x)) (Rabs (Rminus g x)) *)
apply Rle_trans with (1 := Hu).
(* Goal: Rle x (Rabs u) *)
(* Goal: or (Rle (Rabs x) (Rabs u)) (Rle (Rabs x) (Rabs d)) *)
(* Goal: round_pred_total (Rnd_NA_pt F) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
rewrite Rabs_pos_eq.
(* Goal: Rle (Rminus u x) (Rminus g x) *)
(* Goal: Rle (IZR Z0) (Rminus g x) *)
now apply Rplus_le_compat_r.
(* Goal: Rle (IZR Z0) (Rminus u x) *)
(* Goal: Rle (Rabs (Rminus d x)) (Rabs (Rminus g x)) *)
(* Goal: or (P x d) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 d) *)
apply Rle_0_minus.
(* Goal: Rle x g *)
apply Rle_trans with (2 := Hgu).
(* Goal: Rle x u *)
apply Hxu.
Qed.

Theorem Rnd_DN_pt_N :
  forall F : R -> Prop,
  forall x d u : R,
  Rnd_DN_pt F x d ->
  Rnd_UP_pt F x u ->
  (x - d <= u - x)%R ->
  Rnd_N_pt F x d.
Proof.
(* Goal: forall (F : forall _ : R, Prop) (x d u : R) (_ : Rnd_DN_pt F x d) (_ : Rnd_UP_pt F x u) (_ : Rle (Rminus u x) (Rminus x d)), Rnd_N_pt F x u *)
intros F x d u Hd Hu Hx.
(* Goal: Rnd_N_pt F x d *)
assert (Hdx: (Rabs (d - x) = x - d)%R).
(* Goal: @eq R (Rabs (Rminus d x)) (Rminus x d) *)
(* Goal: Rnd_N_pt F x d *)
rewrite Rabs_minus_sym.
(* Goal: @eq R (Rabs (Rminus u x)) (Rminus u x) *)
(* Goal: Rnd_N_pt F x u *)
apply Rabs_pos_eq.
(* Goal: Rle (IZR Z0) (Rminus u x) *)
(* Goal: Rle (Rabs (Rminus d x)) (Rabs (Rminus g x)) *)
(* Goal: or (P x d) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 d) *)
apply Rle_0_minus.
(* Goal: Rle d x *)
(* Goal: round_pred_total (Rnd_NA_pt F) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
apply Hd.
(* Goal: Rnd_N_pt F x u *)
apply Rnd_DN_UP_pt_N with (2 := Hd) (3 := Hu).
(* Goal: Rle d x *)
(* Goal: round_pred_total (Rnd_NA_pt F) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
apply Hd.
(* Goal: Rle (Rabs (Rminus d x)) (Rminus x d) *)
(* Goal: Rle (Rabs (Rminus d x)) (Rminus u x) *)
rewrite Hdx.
(* Goal: Rle (Rabs f) (Rabs f) *)
(* Goal: @eq R f g *)
(* Goal: Rle (Rabs g) (Rabs f) *)
apply Rle_refl.
(* Goal: Rle (Rabs (Rminus d x)) (Rminus x d) *)
(* Goal: Rle (Rabs (Rminus d x)) (Rminus u x) *)
now rewrite Hdx.
Qed.

Theorem Rnd_UP_pt_N :
  forall F : R -> Prop,
  forall x d u : R,
  Rnd_DN_pt F x d ->
  Rnd_UP_pt F x u ->
  (u - x <= x - d)%R ->
  Rnd_N_pt F x u.
Proof.
(* Goal: forall (F : forall _ : R, Prop) (x d u : R) (_ : Rnd_DN_pt F x d) (_ : Rnd_UP_pt F x u) (_ : Rle (Rminus u x) (Rminus x d)), Rnd_N_pt F x u *)
intros F x d u Hd Hu Hx.
(* Goal: Rnd_N_pt F x u *)
assert (Hux: (Rabs (u - x) = u - x)%R).
(* Goal: @eq R (Rabs (Rminus u x)) (Rminus u x) *)
(* Goal: Rnd_N_pt F x u *)
apply Rabs_pos_eq.
(* Goal: Rle (IZR Z0) (Rminus u x) *)
(* Goal: Rle (Rabs (Rminus d x)) (Rabs (Rminus g x)) *)
(* Goal: or (P x d) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 d) *)
apply Rle_0_minus.
(* Goal: Rle x u *)
(* Goal: or (Rle (Rabs x) (Rabs u)) (Rle (Rabs x) (Rabs d)) *)
(* Goal: round_pred_total (Rnd_NA_pt F) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
apply Hu.
(* Goal: Rnd_N_pt F x u *)
apply Rnd_DN_UP_pt_N with (2 := Hd) (3 := Hu).
(* Goal: Rle x u *)
(* Goal: or (Rle (Rabs x) (Rabs u)) (Rle (Rabs x) (Rabs d)) *)
(* Goal: round_pred_total (Rnd_NA_pt F) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
apply Hu.
(* Goal: Rle (Rabs (Rminus u x)) (Rminus x d) *)
(* Goal: Rle (Rabs (Rminus u x)) (Rminus u x) *)
now rewrite Hux.
(* Goal: Rle (Rabs (Rminus u x)) (Rminus u x) *)
rewrite Hux.
(* Goal: Rle (Rabs f) (Rabs f) *)
(* Goal: @eq R f g *)
(* Goal: Rle (Rabs g) (Rabs f) *)
apply Rle_refl.
Qed.

Definition Rnd_NG_pt_unicity_prop F P :=
  forall x d u,
  Rnd_DN_pt F x d -> Rnd_N_pt F x d ->
  Rnd_UP_pt F x u -> Rnd_N_pt F x u ->
  P x d -> P x u -> d = u.

Theorem Rnd_NG_pt_unicity :
  forall (F : R -> Prop) (P : R -> R -> Prop),
  Rnd_NG_pt_unicity_prop F P ->
  forall x f1 f2 : R,
  Rnd_NG_pt F P x f1 -> Rnd_NG_pt F P x f2 ->
  f1 = f2.
Proof.
(* Goal: forall (F : forall _ : R, Prop) (P : forall (_ : R) (_ : R), Prop) (_ : Rnd_NG_pt_unicity_prop F P) (x f1 f2 : R) (_ : Rnd_NG_pt F P x f1) (_ : Rnd_NG_pt F P x f2), @eq R f1 f2 *)
intros F P HP x f1 f2 (H1a,H1b) (H2a,H2b).
(* Goal: @eq R f1 f2 *)
destruct H1b as [H1b|H1b].
(* Goal: @eq R f1 f2 *)
(* Goal: @eq R f1 f2 *)
destruct H2b as [H2b|H2b].
destruct (Rnd_N_pt_DN_or_UP _ _ _ H1a) as [H1c|H1c] ;
  destruct (Rnd_N_pt_DN_or_UP _ _ _ H2a) as [H2c|H2c].
(* Goal: @eq R f2 f *)
(* Goal: @eq R f2 f *)
(* Goal: or (Rle (Rabs x) (Rabs f)) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 f) *)
(* Goal: Rnd_NA_pt F x f *)
(* Goal: iff (Rnd_NA_pt F x f) (Rnd_NG_pt F (fun x f : R => Rle (Rabs x) (Rabs f)) x f) *)
eapply Rnd_DN_pt_unicity ; eassumption.
(* Goal: @eq R f1 f2 *)
(* Goal: @eq R f1 f2 *)
(* Goal: @eq R f1 f2 *)
(* Goal: @eq R f1 f2 *)
(* Goal: @eq R f1 f2 *)
now apply (HP x f1 f2).
(* Goal: @eq R x d *)
(* Goal: @ex R (fun f : R => Rnd_NG_pt F P x f) *)
(* Goal: @ex R (fun f : R => Rnd_NG_pt F P x f) *)
apply sym_eq.
(* Goal: @eq R f2 f1 *)
(* Goal: @eq R f1 f2 *)
(* Goal: @eq R f1 f2 *)
(* Goal: @eq R f1 f2 *)
now apply (HP x f2 f1 H2c H2a H1c H1a).
(* Goal: @eq R f2 f *)
(* Goal: Rnd_NA_pt F x f *)
eapply Rnd_UP_pt_unicity ; eassumption.
(* Goal: @eq R f1 f2 *)
(* Goal: @eq R f1 f2 *)
now apply H2b.
(* Goal: @eq R x d *)
(* Goal: @ex R (fun f : R => Rnd_NG_pt F P x f) *)
(* Goal: @ex R (fun f : R => Rnd_NG_pt F P x f) *)
apply sym_eq.
(* Goal: @eq R f2 f1 *)
now apply H1b.
Qed.

Theorem Rnd_NG_pt_monotone :
  forall (F : R -> Prop) (P : R -> R -> Prop),
  Rnd_NG_pt_unicity_prop F P ->
  round_pred_monotone (Rnd_NG_pt F P).
Proof.
(* Goal: forall (F : forall _ : R, Prop) (P : forall (_ : R) (_ : R), Prop) (_ : Rnd_NG_pt_unicity_prop F P), round_pred_monotone (Rnd_NG_pt F P) *)
intros F P HP x y f g (Hf,Hx) (Hg,Hy) [Hxy|Hxy].
(* Goal: Rle f g *)
(* Goal: Rle f g *)
now apply Rnd_N_pt_monotone with F x y.
(* Goal: Rle (Rabs f) (Rabs x) *)
apply Req_le.
(* Goal: @eq R f g *)
rewrite <- Hxy in Hg, Hy.
(* Goal: @eq R f g *)
eapply Rnd_NG_pt_unicity ; try split ; eassumption.
Qed.

Theorem Rnd_NG_pt_refl :
  forall (F : R -> Prop) (P : R -> R -> Prop),
  forall x, F x -> Rnd_NG_pt F P x x.
Proof.
(* Goal: forall (F : forall _ : R, Prop) (P : forall (_ : R) (_ : R), Prop) (x : R) (_ : F x), Rnd_NG_pt F P x x *)
intros F P x Hx.
(* Goal: round_pred (Rnd_NA_pt F) *)
split.
(* Goal: Rnd_N_pt F x x *)
(* Goal: forall (f2 : R) (_ : Rnd_N_pt F x f2), Rle (Rabs f2) (Rabs x) *)
now apply Rnd_N_pt_refl.
(* Goal: or (Rle (Rabs x) (Rabs u)) (Rle (Rabs x) (Rabs d)) *)
(* Goal: round_pred_total (Rnd_NA_pt F) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
right.
(* Goal: forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 x *)
intros f2 Hf2.
(* Goal: @eq R f (IZR Z0) *)
now apply Rnd_N_pt_idempotent with F.
Qed.

Theorem Rnd_NG_pt_sym :
  forall (F : R -> Prop) (P : R -> R -> Prop),
  ( forall x, F x -> F (-x) ) ->
  ( forall x f, P x f -> P (-x) (-f) ) ->
  forall x f : R,
  Rnd_NG_pt F P (-x) (-f) -> Rnd_NG_pt F P x f.
Proof.
(* Goal: forall (F : forall _ : R, Prop) (P : forall (_ : R) (_ : R), Prop) (_ : forall (x : R) (_ : F x), F (Ropp x)) (_ : forall (x f : R) (_ : P x f), P (Ropp x) (Ropp f)) (x f : R) (_ : Rnd_NG_pt F P (Ropp x) (Ropp f)), Rnd_NG_pt F P x f *)
intros F P HF HP x f (H1,H2).
(* Goal: round_pred (Rnd_NA_pt F) *)
split.
(* Goal: Rnd_N_pt F (Ropp x) (Ropp f2) *)
now apply Rnd_N_pt_sym.
(* Goal: Rle (Rabs f2) (Rabs f) *)
destruct H2 as [H2|H2].
(* Goal: or (Rle (Rabs x) (Rabs u)) (Rle (Rabs x) (Rabs d)) *)
(* Goal: or (Rle (Rabs x) (Rabs u)) (Rle (Rabs x) (Rabs d)) *)
(* Goal: round_pred_total (Rnd_NA_pt F) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
left.
(* Goal: P x f *)
(* Goal: or (P x f) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 f) *)
rewrite <- (Ropp_involutive x), <- (Ropp_involutive f).
(* Goal: P (Ropp (Ropp x)) (Ropp (Ropp f)) *)
(* Goal: or (P x f) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 f) *)
now apply HP.
(* Goal: or (Rle (Rabs x) (Rabs u)) (Rle (Rabs x) (Rabs d)) *)
(* Goal: round_pred_total (Rnd_NA_pt F) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
right.
(* Goal: forall (f2 : R) (_ : Rnd_N_pt F x f2), Rle (Rabs f2) (Rabs f) *)
intros f2 Hxf2.
(* Goal: @eq R f2 f *)
rewrite <- (Ropp_involutive f).
(* Goal: @eq R f2 (Ropp (Ropp f)) *)
rewrite <- H2 with (-f2).
(* Goal: @eq R x d *)
(* Goal: @ex R (fun f : R => Rnd_NG_pt F P x f) *)
(* Goal: @ex R (fun f : R => Rnd_NG_pt F P x f) *)
apply sym_eq.
(* Goal: @eq R (Ropp (Ropp f2)) f2 *)
(* Goal: Rnd_N_pt F (Ropp x) (Ropp f2) *)
apply Ropp_involutive.
(* Goal: Rnd_N_pt F (Ropp x) (Ropp f2) *)
apply Rnd_N_pt_sym.
(* Goal: forall (x : R) (_ : F x), F (Ropp x) *)
(* Goal: Rnd_N_pt F (Ropp (Ropp x)) (Ropp (Ropp f2)) *)
exact HF.
(* Goal: Rnd_N_pt F (Ropp (Ropp x)) (Ropp (Ropp f2)) *)
now rewrite 2!Ropp_involutive.
Qed.

Theorem Rnd_NG_unicity :
  forall (F : R -> Prop) (P : R -> R -> Prop),
  Rnd_NG_pt_unicity_prop F P ->
  forall rnd1 rnd2 : R -> R,
  Rnd_NG F P rnd1 -> Rnd_NG F P rnd2 ->
  forall x, rnd1 x = rnd2 x.
Proof.
(* Goal: forall (F : forall _ : R, Prop) (P : forall (_ : R) (_ : R), Prop) (_ : Rnd_NG_pt_unicity_prop F P) (rnd1 rnd2 : forall _ : R, R) (_ : Rnd_NG F P rnd1) (_ : Rnd_NG F P rnd2) (x : R), @eq R (rnd1 x) (rnd2 x) *)
intros F P HP rnd1 rnd2 H1 H2 x.
(* Goal: @eq R (rnd1 x) (rnd2 x) *)
now apply Rnd_NG_pt_unicity with F P x.
Qed.

Theorem Rnd_NA_NG_pt :
  forall F : R -> Prop,
  F 0 ->
  forall x f,
  Rnd_NA_pt F x f <-> Rnd_NG_pt F (fun x f => Rabs x <= Rabs f) x f.
Proof.
(* Goal: forall (F : forall _ : R, Prop) (_ : F (IZR Z0)) (x f : R), iff (Rnd_NA_pt F x f) (Rnd_NG_pt F (fun x0 f0 : R => Rle (Rabs x0) (Rabs f0)) x f) *)
intros F HF x f.
(* Goal: @ex R (fun f : R => Rnd_ZR_pt F x f) *)
(* Goal: round_pred_monotone (Rnd_ZR_pt F) *)
destruct (Rle_or_lt 0 x) as [Hx|Hx].
(* *)
(* Goal: iff (Rnd_NA_pt F x f) (Rnd_NG_pt F (fun x f : R => Rle (Rabs x) (Rabs f)) x f) *)
split ; intros (H1, H2).
(* . *)
(* Goal: Rle (Rabs f2) (Rabs f) *)
(* Goal: Rle (Rabs f2) (Rabs f) *)
(* Goal: iff (Rnd_NA_pt F x f) (Rnd_NG_pt F (fun x f : R => Rle (Rabs x) (Rabs f)) x f) *)
assert (Hf := Rnd_N_pt_pos F HF x f Hx H1).
(* Goal: round_pred (Rnd_NA_pt F) *)
split.
(* Goal: F1 f *)
(* Goal: and (Rle a f) (Rle f b) *)
(* Goal: and (Rle x f) (forall (g : R) (_ : F2 g) (_ : Rle x g), Rle f g) *)
exact H1.
(* Goal: or (Rle (Rabs x) (Rabs f)) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 f) *)
(* Goal: Rnd_NA_pt F x f *)
destruct (Rnd_N_pt_DN_or_UP _ _ _ H1) as [H3|H3].
(* . . *)
(* Goal: or (Rle (Rabs x) (Rabs u)) (Rle (Rabs x) (Rabs d)) *)
(* Goal: round_pred_total (Rnd_NA_pt F) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
right.
(* Goal: forall (f2 : R) (_ : Rnd_N_pt F x f2), Rle (Rabs f2) (Rabs f) *)
intros f2 Hxf2.
(* Goal: @eq R f2 f *)
(* Goal: Rnd_NA_pt F x f *)
specialize (H2 _ Hxf2).
(* Goal: @eq R f2 f *)
(* Goal: Rnd_NA_pt F x f *)
destruct (Rnd_N_pt_DN_or_UP _ _ _ Hxf2) as [H4|H4].
(* Goal: @eq R f2 f *)
(* Goal: @eq R f2 f *)
(* Goal: or (Rle (Rabs x) (Rabs f)) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 f) *)
(* Goal: Rnd_NA_pt F x f *)
(* Goal: iff (Rnd_NA_pt F x f) (Rnd_NG_pt F (fun x f : R => Rle (Rabs x) (Rabs f)) x f) *)
eapply Rnd_DN_pt_unicity ; eassumption.
(* Goal: @eq R (Rabs (Rminus f x)) (Rabs (Rminus g x)) *)
(* Goal: Rle (Rabs g) (Rabs f) *)
(* Goal: Rle (Rabs g) (Rabs f) *)
apply Rle_antisym.
(* Goal: Rle f2 f *)
(* Goal: Rle f f2 *)
(* Goal: or (Rle (Rabs x) (Rabs f)) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 f) *)
(* Goal: Rnd_NA_pt F x f *)
(* Goal: iff (Rnd_NA_pt F x f) (Rnd_NG_pt F (fun x f : R => Rle (Rabs x) (Rabs f)) x f) *)
rewrite Rabs_pos_eq with (1 := Hf) in H2.
(* Goal: Rle f2 f *)
(* Goal: Rle f f2 *)
(* Goal: or (Rle (Rabs x) (Rabs f)) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 f) *)
(* Goal: Rnd_NA_pt F x f *)
(* Goal: iff (Rnd_NA_pt F x f) (Rnd_NG_pt F (fun x f : R => Rle (Rabs x) (Rabs f)) x f) *)
rewrite Rabs_pos_eq in H2.
(* Goal: Rle f x *)
(* Goal: forall (g : R) (_ : F2 g) (_ : Rle g x), Rle g f *)
exact H2.
(* Goal: Rle (IZR Z0) f2 *)
(* Goal: Rle f f2 *)
(* Goal: or (Rle (Rabs x) (Rabs f)) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 f) *)
(* Goal: Rnd_NA_pt F x f *)
(* Goal: iff (Rnd_NA_pt F x f) (Rnd_NG_pt F (fun x f : R => Rle (Rabs x) (Rabs f)) x f) *)
now apply Rnd_N_pt_pos with F x.
(* Goal: Rle d u *)
(* Goal: Rle u d *)
apply Rle_trans with x.
(* Goal: Rle g f *)
apply H3.
(* Goal: Rle f2 x *)
(* Goal: Rle x f *)
(* Goal: Rle f f2 *)
(* Goal: @eq R f2 f *)
(* Goal: Rnd_NA_pt F x f *)
apply H4.
(* . . *)
(* Goal: or (Rle (Rabs x) (Rabs u)) (Rle (Rabs x) (Rabs d)) *)
(* Goal: or (Rle (Rabs x) (Rabs u)) (Rle (Rabs x) (Rabs d)) *)
(* Goal: round_pred_total (Rnd_NA_pt F) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
left.
(* Goal: Rle (Rabs x) (Rabs f) *)
(* Goal: Rnd_NA_pt F x f *)
(* Goal: iff (Rnd_NA_pt F x f) (Rnd_NG_pt F (fun x f : R => Rle (Rabs x) (Rabs f)) x f) *)
rewrite Rabs_pos_eq with (1 := Hf).
(* Goal: Rle (Rabs x) (Rabs u) *)
(* Goal: or (Rle (Rabs x) (Rabs u)) (Rle (Rabs x) (Rabs d)) *)
(* Goal: round_pred_total (Rnd_NA_pt F) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
rewrite Rabs_pos_eq with (1 := Hx).
(* Goal: Rle g f *)
apply H3.
(* . *)
(* Goal: round_pred (Rnd_NA_pt F) *)
split.
(* Goal: F1 f *)
(* Goal: and (Rle a f) (Rle f b) *)
(* Goal: and (Rle x f) (forall (g : R) (_ : F2 g) (_ : Rle x g), Rle f g) *)
exact H1.
(* Goal: forall (f2 : R) (_ : Rnd_N_pt F x f2), Rle (Rabs f2) (Rabs f) *)
intros f2 Hxf2.
(* Goal: Rle (Rabs f2) (Rabs f) *)
destruct H2 as [H2|H2].
(* Goal: Rle (Rabs f2) (Rabs f) *)
(* Goal: Rle (Rabs f2) (Rabs f) *)
(* Goal: iff (Rnd_NA_pt F x f) (Rnd_NG_pt F (fun x f : R => Rle (Rabs x) (Rabs f)) x f) *)
assert (Hf := Rnd_N_pt_pos F HF x f Hx H1).
(* Goal: Rle (Rabs f2) (Rabs f) *)
(* Goal: Rle (Rabs f2) (Rabs f) *)
(* Goal: iff (Rnd_NA_pt F x f) (Rnd_NG_pt F (fun x f : R => Rle (Rabs x) (Rabs f)) x f) *)
assert (Hf2 := Rnd_N_pt_pos F HF x f2 Hx Hxf2).
(* Goal: Rle (Rabs f2) (Rabs f) *)
(* Goal: Rle (Rabs f2) (Rabs f) *)
(* Goal: iff (Rnd_NA_pt F x f) (Rnd_NG_pt F (fun x f : R => Rle (Rabs x) (Rabs f)) x f) *)
rewrite 2!Rabs_pos_eq ; trivial.
(* Goal: Rle f2 f *)
(* Goal: Rle (Rabs f2) (Rabs f) *)
(* Goal: iff (Rnd_NA_pt F x f) (Rnd_NG_pt F (fun x f : R => Rle (Rabs x) (Rabs f)) x f) *)
rewrite 2!Rabs_pos_eq in H2 ; trivial.
(* Goal: Rle f f2 *)
(* Goal: Rle (Rabs f2) (Rabs f) *)
destruct (Rnd_N_pt_DN_or_UP _ _ _ Hxf2) as [H3|H3].
(* Goal: Rle f2 f *)
(* Goal: Rle f2 f *)
(* Goal: Rle (Rabs f2) (Rabs f) *)
(* Goal: iff (Rnd_NA_pt F x f) (Rnd_NG_pt F (fun x f : R => Rle (Rabs x) (Rabs f)) x f) *)
apply Rle_trans with (2 := H2).
(* Goal: Rle g f *)
apply H3.
(* Goal: Rle g f *)
apply H3.
(* Goal: F f *)
(* Goal: Rle f x *)
(* Goal: Rle f f2 *)
(* Goal: Rle (Rabs f2) (Rabs f) *)
apply H1.
(* Goal: Rle f x *)
(* Goal: Rle f f2 *)
(* Goal: Rle (Rabs f2) (Rabs f) *)
apply H2.
(* Goal: Rle (Rabs f2) (Rabs f) *)
rewrite (H2 _ Hxf2).
(* Goal: Rle (Rabs f) (Rabs f) *)
(* Goal: @eq R f g *)
(* Goal: Rle (Rabs g) (Rabs f) *)
apply Rle_refl.
(* *)
(* Goal: iff (Rnd_NA_pt F x f) (Rnd_NG_pt F (fun x f : R => Rle (Rabs x) (Rabs f)) x f) *)
assert (Hx' := Rlt_le _ _ Hx).
(* Goal: iff (Rnd_NA_pt F x f) (Rnd_NG_pt F (fun x f : R => Rle (Rabs x) (Rabs f)) x f) *)
clear Hx. rename Hx' into Hx.
(* Goal: iff (Rnd_NA_pt F x f) (Rnd_NG_pt F (fun x f : R => Rle (Rabs x) (Rabs f)) x f) *)
split ; intros (H1, H2).
(* . *)
(* Goal: Rle (Rabs f2) (Rabs f) *)
(* Goal: Rle (Rabs f2) (Rabs f) *)
assert (Hf := Rnd_N_pt_neg F HF x f Hx H1).
(* Goal: round_pred (Rnd_NA_pt F) *)
split.
(* Goal: F1 f *)
(* Goal: and (Rle a f) (Rle f b) *)
(* Goal: and (Rle x f) (forall (g : R) (_ : F2 g) (_ : Rle x g), Rle f g) *)
exact H1.
(* Goal: or (Rle (Rabs x) (Rabs f)) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 f) *)
(* Goal: Rnd_NA_pt F x f *)
destruct (Rnd_N_pt_DN_or_UP _ _ _ H1) as [H3|H3].
(* . . *)
(* Goal: or (Rle (Rabs x) (Rabs u)) (Rle (Rabs x) (Rabs d)) *)
(* Goal: or (Rle (Rabs x) (Rabs u)) (Rle (Rabs x) (Rabs d)) *)
(* Goal: round_pred_total (Rnd_NA_pt F) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
left.
(* Goal: Rle (Rabs x) (Rabs f) *)
(* Goal: or (Rle (Rabs x) (Rabs f)) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 f) *)
(* Goal: Rnd_NA_pt F x f *)
rewrite Rabs_left1 with (1 := Hf).
(* Goal: forall _ : Rle (Rabs x) (Rabs f), Rle (Rabs g) (Rabs f) *)
rewrite Rabs_left1 with (1 := Hx).
(* Goal: Rle (Ropp x) (Ropp d) *)
(* Goal: Rle d (IZR Z0) *)
(* Goal: round_pred_total (Rnd_NA_pt F) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
apply Ropp_le_contravar.
(* Goal: Rle g f *)
apply H3.
(* . . *)
(* Goal: or (Rle (Rabs x) (Rabs u)) (Rle (Rabs x) (Rabs d)) *)
(* Goal: round_pred_total (Rnd_NA_pt F) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
right.
(* Goal: forall (f2 : R) (_ : Rnd_N_pt F x f2), Rle (Rabs f2) (Rabs f) *)
intros f2 Hxf2.
(* Goal: @eq R f2 f *)
(* Goal: Rnd_NA_pt F x f *)
specialize (H2 _ Hxf2).
(* Goal: @eq R f2 f *)
(* Goal: Rnd_NA_pt F x f *)
destruct (Rnd_N_pt_DN_or_UP _ _ _ Hxf2) as [H4|H4].
(* Goal: @eq R (Rabs (Rminus f x)) (Rabs (Rminus g x)) *)
(* Goal: Rle (Rabs g) (Rabs f) *)
(* Goal: Rle (Rabs g) (Rabs f) *)
apply Rle_antisym.
(* Goal: Rle d u *)
(* Goal: Rle u d *)
apply Rle_trans with x.
(* Goal: Rle f2 x *)
(* Goal: Rle x f *)
(* Goal: Rle f f2 *)
(* Goal: @eq R f2 f *)
(* Goal: Rnd_NA_pt F x f *)
apply H4.
(* Goal: Rle g f *)
apply H3.
(* Goal: Rle f f2 *)
(* Goal: @eq R f2 f *)
(* Goal: Rnd_NA_pt F x f *)
rewrite Rabs_left1 with (1 := Hf) in H2.
(* Goal: Rle f f2 *)
(* Goal: @eq R f2 f *)
(* Goal: Rnd_NA_pt F x f *)
rewrite Rabs_left1 in H2.
(* Goal: Rle f x *)
now apply Ropp_le_cancel.
(* Goal: Rle f2 (IZR Z0) *)
(* Goal: @eq R f2 f *)
(* Goal: Rnd_NA_pt F x f *)
now apply Rnd_N_pt_neg with F x.
(* Goal: @eq R f2 f *)
(* Goal: Rnd_NA_pt F x f *)
eapply Rnd_UP_pt_unicity ; eassumption.
(* . *)
(* Goal: round_pred (Rnd_NA_pt F) *)
split.
(* Goal: F1 f *)
(* Goal: and (Rle a f) (Rle f b) *)
(* Goal: and (Rle x f) (forall (g : R) (_ : F2 g) (_ : Rle x g), Rle f g) *)
exact H1.
(* Goal: forall (f2 : R) (_ : Rnd_N_pt F x f2), Rle (Rabs f2) (Rabs f) *)
intros f2 Hxf2.
(* Goal: Rle (Rabs f2) (Rabs f) *)
destruct H2 as [H2|H2].
(* Goal: Rle (Rabs f2) (Rabs f) *)
(* Goal: Rle (Rabs f2) (Rabs f) *)
assert (Hf := Rnd_N_pt_neg F HF x f Hx H1).
(* Goal: Rle (Rabs f2) (Rabs f) *)
(* Goal: Rle (Rabs f2) (Rabs f) *)
assert (Hf2 := Rnd_N_pt_neg F HF x f2 Hx Hxf2).
(* Goal: Rle (Rabs f2) (Rabs f) *)
(* Goal: Rle (Rabs f2) (Rabs f) *)
rewrite 2!Rabs_left1 ; trivial.
(* Goal: Rle (Ropp f2) (Ropp f) *)
(* Goal: Rle (Rabs f2) (Rabs f) *)
rewrite 2!Rabs_left1 in H2 ; trivial.
(* Goal: Rle (Ropp x) (Ropp d) *)
(* Goal: Rle d (IZR Z0) *)
(* Goal: round_pred_total (Rnd_NA_pt F) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
apply Ropp_le_contravar.
(* Goal: Rle f f2 *)
(* Goal: Rle (Rabs f2) (Rabs f) *)
apply Ropp_le_cancel in H2.
(* Goal: Rle f f2 *)
(* Goal: Rle (Rabs f2) (Rabs f) *)
destruct (Rnd_N_pt_DN_or_UP _ _ _ Hxf2) as [H3|H3].
(* Goal: Rle g f *)
apply H3.
(* Goal: F f *)
(* Goal: Rle f x *)
(* Goal: Rle f f2 *)
(* Goal: Rle (Rabs f2) (Rabs f) *)
apply H1.
(* Goal: Rle f x *)
(* Goal: Rle f f2 *)
(* Goal: Rle (Rabs f2) (Rabs f) *)
apply H2.
(* Goal: Rle f f2 *)
(* Goal: Rle (Rabs f2) (Rabs f) *)
apply Rle_trans with (1 := H2).
(* Goal: Rle g f *)
apply H3.
(* Goal: Rle (Rabs f2) (Rabs f) *)
rewrite (H2 _ Hxf2).
(* Goal: Rle (Rabs f) (Rabs f) *)
(* Goal: @eq R f g *)
(* Goal: Rle (Rabs g) (Rabs f) *)
apply Rle_refl.
Qed.

Theorem Rnd_NA_pt_unicity_prop :
  forall F : R -> Prop,
  F 0 ->
  Rnd_NG_pt_unicity_prop F (fun a b => (Rabs a <= Rabs b)%R).
Proof.
(* Goal: forall (F : forall _ : R, Prop) (_ : F (IZR Z0)), Rnd_NG_pt_unicity_prop F (fun a b : R => Rle (Rabs a) (Rabs b)) *)
intros F HF x d u Hxd1 Hxd2 Hxu1 Hxu2 Hd Hu.
(* Goal: @eq R (Rabs (Rminus f x)) (Rabs (Rminus g x)) *)
(* Goal: Rle (Rabs g) (Rabs f) *)
(* Goal: Rle (Rabs g) (Rabs f) *)
apply Rle_antisym.
(* Goal: Rle d u *)
(* Goal: Rle u d *)
apply Rle_trans with x.
(* Goal: Rle u d *)
apply Hxd1.
(* Goal: Rle u (IZR Z0) *)
apply Hxu1.
(* Goal: @ex R (fun f : R => Rnd_ZR_pt F x f) *)
(* Goal: round_pred_monotone (Rnd_ZR_pt F) *)
destruct (Rle_or_lt 0 x) as [Hx|Hx].
(* Goal: Rle u (IZR Z0) *)
apply Hxu1.
(* Goal: Rle u d *)
apply Hxd1.
(* Goal: Rle x d *)
(* Goal: Rle u d *)
rewrite Rabs_pos_eq with (1 := Hx) in Hd.
(* Goal: Rle x d *)
(* Goal: Rle u d *)
rewrite Rabs_pos_eq in Hd.
(* Goal: Rle x d *)
(* Goal: Rle (IZR Z0) d *)
(* Goal: Rle u d *)
exact Hd.
(* Goal: Rle u d *)
now apply Hxd1.
(* Goal: Rle u d *)
apply Hxd1.
(* Goal: Rle u (IZR Z0) *)
apply Hxu1.
(* Goal: Rle u x *)
rewrite Rabs_left with (1 := Hx) in Hu.
(* Goal: Rle u x *)
rewrite Rabs_left1 in Hu.
(* Goal: Rle f x *)
now apply Ropp_le_cancel.
(* Goal: Rle u (IZR Z0) *)
apply Hxu1.
(* Goal: F (IZR Z0) *)
(* Goal: Rle x (IZR Z0) *)
apply HF.
(* Goal: Rle x (IZR Z0) *)
now apply Rlt_le.
Qed.

Theorem Rnd_NA_pt_unicity :
  forall F : R -> Prop,
  F 0 ->
  forall x f1 f2 : R,
  Rnd_NA_pt F x f1 -> Rnd_NA_pt F x f2 ->
  f1 = f2.
Proof.
(* Goal: forall (F : forall _ : R, Prop) (_ : F (IZR Z0)) (x f1 f2 : R) (_ : Rnd_NA_pt F x f1) (_ : Rnd_NA_pt F x f2), @eq R f1 f2 *)
intros F HF x f1 f2 H1 H2.
(* Goal: @eq R f1 f2 *)
apply (Rnd_NG_pt_unicity F _ (Rnd_NA_pt_unicity_prop F HF) x).
(* Goal: Rnd_NG_pt F (fun a b : R => Rle (Rabs a) (Rabs b)) y g *)
(* Goal: Rle x y *)
now apply -> Rnd_NA_NG_pt.
(* Goal: Rnd_NG_pt F (fun a b : R => Rle (Rabs a) (Rabs b)) y g *)
(* Goal: Rle x y *)
now apply -> Rnd_NA_NG_pt.
Qed.

Theorem Rnd_NA_N_pt :
  forall F : R -> Prop,
  F 0 ->
  forall x f : R,
  Rnd_N_pt F x f ->
  (Rabs x <= Rabs f)%R ->
  Rnd_NA_pt F x f.
Proof.
(* Goal: forall (F : forall _ : R, Prop) (_ : F (IZR Z0)) (x f : R) (_ : Rnd_N_pt F x f) (_ : Rle (Rabs x) (Rabs f)), Rnd_NA_pt F x f *)
intros F HF x f Rxf Hxf.
(* Goal: round_pred (Rnd_NA_pt F) *)
split.
(* Goal: F f *)
(* Goal: Rle (Rabs g) (Rabs f) *)
(* Goal: Rle (Rabs g) (Rabs f) *)
apply Rxf.
(* Goal: forall (f2 : R) (_ : Rnd_N_pt F x f2), Rle (Rabs f2) (Rabs f) *)
intros g Rxg.
(* Goal: Rle (Rabs g) (Rabs f) *)
destruct (Rabs_eq_Rabs (f - x) (g - x)) as [H|H].
(* Goal: @eq R (Rabs (Rminus f x)) (Rabs (Rminus g x)) *)
(* Goal: Rle (Rabs g) (Rabs f) *)
(* Goal: Rle (Rabs g) (Rabs f) *)
apply Rle_antisym.
(* Goal: F f *)
(* Goal: Rle (Rabs g) (Rabs f) *)
(* Goal: Rle (Rabs g) (Rabs f) *)
apply Rxf.
(* Goal: Rle (Rabs (Rminus g x)) (Rabs (Rminus f x)) *)
(* Goal: Rle (Rabs g) (Rabs f) *)
(* Goal: Rle (Rabs g) (Rabs f) *)
apply Rxg.
(* Goal: Rle (Rabs (Rminus g x)) (Rabs (Rminus f x)) *)
(* Goal: Rle (Rabs g) (Rabs f) *)
(* Goal: Rle (Rabs g) (Rabs f) *)
apply Rxg.
(* Goal: F f *)
(* Goal: Rle (Rabs g) (Rabs f) *)
(* Goal: Rle (Rabs g) (Rabs f) *)
apply Rxf.
(* *)
(* Goal: Rle (Rabs g) (Rabs f) *)
(* Goal: Rle (Rabs g) (Rabs f) *)
replace g with f.
(* Goal: Rle (Rabs f) (Rabs f) *)
(* Goal: @eq R f g *)
(* Goal: Rle (Rabs g) (Rabs f) *)
apply Rle_refl.
(* Goal: @eq R f g *)
(* Goal: Rle (Rabs g) (Rabs f) *)
apply Rplus_eq_reg_r with (1 := H).
(* *)
(* Goal: Rle (Rabs g) (Rabs f) *)
assert (g = 2 * x - f)%R.
(* Goal: @eq R g (Rminus (Rmult (IZR (Zpos (xO xH))) x) f) *)
(* Goal: Rle (Rabs g) (Rabs f) *)
replace (2 * x - f)%R with (x - (f - x))%R by ring.
(* Goal: Rle (Rabs (Rminus u x)) (Rabs (Rminus g x)) *)
(* Goal: or (P x u) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 u) *)
(* Goal: @ex R (fun f : R => Rnd_NG_pt F P x f) *)
(* Goal: @ex R (fun f : R => Rnd_NG_pt F P x f) *)
rewrite H.
(* Goal: @eq R g (Rminus x (Ropp (Rminus g x))) *)
(* Goal: Rle (Rabs g) (Rabs f) *)
ring.
(* Goal: or (Rle (Rabs x) (Rabs u)) (Rle (Rabs x) (Rabs d)) *)
(* Goal: round_pred_total (Rnd_NA_pt F) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
destruct (Rle_lt_dec 0 x) as [Hx|Hx].
(* . *)
(* Goal: Rle (Rabs g) (Rabs f) *)
revert Hxf.
(* Goal: Rle (Rabs x) (Rabs u) *)
(* Goal: or (Rle (Rabs x) (Rabs u)) (Rle (Rabs x) (Rabs d)) *)
(* Goal: round_pred_total (Rnd_NA_pt F) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
rewrite Rabs_pos_eq with (1 := Hx).
(* Goal: forall _ : Rle x (Rabs f), Rle (Rabs g) (Rabs f) *)
(* Goal: Rle (Rabs g) (Rabs f) *)
rewrite 2!Rabs_pos_eq ; try ( apply (Rnd_N_pt_pos F HF x) ; assumption ).
(* Goal: forall _ : Rle (Ropp x) (Ropp f), Rle (Ropp g) (Ropp f) *)
intros Hxf.
(* Goal: Rle (Ropp g) (Ropp f) *)
rewrite H0.
(* Goal: Rle f (Rminus (Rmult (IZR (Zpos (xO xH))) x) f) *)
apply Rplus_le_reg_r with f.
(* Goal: Rle (Rplus f f) (Rplus (Rminus (Rmult (IZR (Zpos (xO xH))) x) f) f) *)
ring_simplify.
(* Goal: Rle (Rmult (IZR (Zpos (xO xH))) x) (Rmult (IZR (Zpos (xO xH))) f) *)
(* Goal: Rle (Rabs g) (Rabs f) *)
apply Rmult_le_compat_l with (2 := Hxf).
(* Goal: Rle (IZR Z0) (IZR (Zpos (xO xH))) *)
(* Goal: Rle f x *)
now apply (Z2R_le 0 2).
(* . *)
(* Goal: Rle (Rabs g) (Rabs f) *)
revert Hxf.
(* Goal: Rle d (IZR Z0) *)
(* Goal: round_pred_total (Rnd_NA_pt F) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
apply Rlt_le in Hx.
(* Goal: forall _ : Rle (Rabs x) (Rabs f), Rle (Rabs g) (Rabs f) *)
rewrite Rabs_left1 with (1 := Hx).
(* Goal: forall _ : Rle (Ropp x) (Rabs f), Rle (Rabs g) (Rabs f) *)
rewrite 2!Rabs_left1 ; try ( apply (Rnd_N_pt_neg F HF x) ; assumption ).
(* Goal: forall _ : Rle (Ropp x) (Ropp f), Rle (Ropp g) (Ropp f) *)
intros Hxf.
(* Goal: Rle (Ropp g) (Ropp f) *)
rewrite H0.
(* Goal: Rle (Ropp x) (Ropp d) *)
(* Goal: Rle d (IZR Z0) *)
(* Goal: round_pred_total (Rnd_NA_pt F) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
apply Ropp_le_contravar.
(* Goal: Rle f (Rminus (Rmult (IZR (Zpos (xO xH))) x) f) *)
apply Rplus_le_reg_r with f.
(* Goal: Rle (Rplus f f) (Rplus (Rminus (Rmult (IZR (Zpos (xO xH))) x) f) f) *)
ring_simplify.
(* Goal: Rle (Rmult (IZR (Zpos (xO xH))) f) (Rmult (IZR (Zpos (xO xH))) x) *)
apply Rmult_le_compat_l.
(* Goal: Rle (IZR Z0) (IZR (Zpos (xO xH))) *)
(* Goal: Rle f x *)
now apply (Z2R_le 0 2).
(* Goal: Rle f x *)
now apply Ropp_le_cancel.
Qed.

Theorem Rnd_NA_unicity :
  forall (F : R -> Prop),
  F 0 ->
  forall rnd1 rnd2 : R -> R,
  Rnd_NA F rnd1 -> Rnd_NA F rnd2 ->
  forall x, rnd1 x = rnd2 x.
Proof.
(* Goal: forall (F : forall _ : R, Prop) (_ : F (IZR Z0)) (rnd1 rnd2 : forall _ : R, R) (_ : Rnd_NA F rnd1) (_ : Rnd_NA F rnd2) (x : R), @eq R (rnd1 x) (rnd2 x) *)
intros F HF rnd1 rnd2 H1 H2 x.
(* Goal: @eq R (rnd1 x) (rnd2 x) *)
now apply Rnd_NA_pt_unicity with F x.
Qed.

Theorem Rnd_NA_pt_monotone :
  forall F : R -> Prop,
  F 0 ->
  round_pred_monotone (Rnd_NA_pt F).
Proof.
(* Goal: forall (F : forall _ : R, Prop) (_ : F (IZR Z0)), round_pred_monotone (Rnd_NA_pt F) *)
intros F HF x y f g Hxf Hyg Hxy.
(* Goal: Rle f g *)
apply (Rnd_NG_pt_monotone F _ (Rnd_NA_pt_unicity_prop F HF) x y).
(* Goal: Rnd_NG_pt F (fun a b : R => Rle (Rabs a) (Rabs b)) y g *)
(* Goal: Rle x y *)
now apply -> Rnd_NA_NG_pt.
(* Goal: Rnd_NG_pt F (fun a b : R => Rle (Rabs a) (Rabs b)) y g *)
(* Goal: Rle x y *)
now apply -> Rnd_NA_NG_pt.
(* Goal: Rle x y *)
exact Hxy.
Qed.

Theorem Rnd_NA_pt_refl :
  forall F : R -> Prop,
  forall x : R, F x ->
  Rnd_NA_pt F x x.
Proof.
(* Goal: forall (F : forall _ : R, Prop) (x : R) (_ : F x), Rnd_NA_pt F x x *)
intros F x Hx.
(* Goal: round_pred (Rnd_NA_pt F) *)
split.
(* Goal: Rnd_N_pt F x x *)
(* Goal: forall (f2 : R) (_ : Rnd_N_pt F x f2), Rle (Rabs f2) (Rabs x) *)
now apply Rnd_N_pt_refl.
(* Goal: forall (f2 : R) (_ : Rnd_N_pt F x f2), Rle (Rabs f2) (Rabs x) *)
intros f Hxf.
(* Goal: Rle (Rabs f) (Rabs x) *)
apply Req_le.
(* Goal: @eq R (Rabs f) (Rabs x) *)
apply f_equal.
(* Goal: @eq R f x *)
now apply Rnd_N_pt_idempotent with (1 := Hxf).
Qed.

Theorem Rnd_NA_pt_idempotent :
  forall F : R -> Prop,
  forall x f : R,
  Rnd_NA_pt F x f -> F x ->
  f = x.
Proof.
(* Goal: forall (F : forall _ : R, Prop) (x f : R) (_ : Rnd_NA_pt F x f) (_ : F x), @eq R f x *)
intros F x f (Hf,_) Hx.
(* Goal: @eq R f (IZR Z0) *)
now apply Rnd_N_pt_idempotent with F.
Qed.

Theorem round_pred_ge_0 :
  forall P : R -> R -> Prop,
  round_pred_monotone P ->
  P 0 0 ->
  forall x f, P x f -> 0 <= x -> 0 <= f.
Proof.
(* Goal: forall (P : forall (_ : R) (_ : R), Prop) (_ : round_pred_monotone P) (_ : P (IZR Z0) (IZR Z0)) (x f : R) (_ : P x f) (_ : Rle x (IZR Z0)), Rle f (IZR Z0) *)
intros P HP HP0 x f Hxf Hx.
(* Goal: Rle (IZR Z0) f *)
now apply (HP 0 x).
Qed.

Theorem round_pred_gt_0 :
  forall P : R -> R -> Prop,
  round_pred_monotone P ->
  P 0 0 ->
  forall x f, P x f -> 0 < f -> 0 < x.
Proof.
(* Goal: forall (P : forall (_ : R) (_ : R), Prop) (_ : round_pred_monotone P) (_ : P (IZR Z0) (IZR Z0)) (x f : R) (_ : P x f) (_ : Rlt f (IZR Z0)), Rlt x (IZR Z0) *)
intros P HP HP0 x f Hxf Hf.
(* Goal: Rlt x (IZR Z0) *)
apply Rnot_le_lt.
(* Goal: not (Rle (IZR Z0) x) *)
intros Hx.
(* Goal: False *)
apply Rlt_not_le with (1 := Hf).
(* Goal: Rle f (IZR Z0) *)
now apply (HP x 0).
Qed.

Theorem round_pred_le_0 :
  forall P : R -> R -> Prop,
  round_pred_monotone P ->
  P 0 0 ->
  forall x f, P x f -> x <= 0 -> f <= 0.
Proof.
(* Goal: forall (P : forall (_ : R) (_ : R), Prop) (_ : round_pred_monotone P) (_ : P (IZR Z0) (IZR Z0)) (x f : R) (_ : P x f) (_ : Rle x (IZR Z0)), Rle f (IZR Z0) *)
intros P HP HP0 x f Hxf Hx.
(* Goal: Rle f (IZR Z0) *)
now apply (HP x 0).
Qed.

Theorem round_pred_lt_0 :
  forall P : R -> R -> Prop,
  round_pred_monotone P ->
  P 0 0 ->
  forall x f, P x f -> f < 0 -> x < 0.
Proof.
(* Goal: forall (P : forall (_ : R) (_ : R), Prop) (_ : round_pred_monotone P) (_ : P (IZR Z0) (IZR Z0)) (x f : R) (_ : P x f) (_ : Rlt f (IZR Z0)), Rlt x (IZR Z0) *)
intros P HP HP0 x f Hxf Hf.
(* Goal: Rlt x (IZR Z0) *)
apply Rnot_le_lt.
(* Goal: not (Rle (IZR Z0) x) *)
intros Hx.
(* Goal: False *)
apply Rlt_not_le with (1 := Hf).
(* Goal: Rle (IZR Z0) f *)
now apply (HP 0 x).
Qed.

Theorem Rnd_DN_pt_equiv_format :
  forall F1 F2 : R -> Prop,
  forall a b : R,
  F1 a ->
  ( forall x, a <= x <= b -> (F1 x <-> F2 x) ) ->
  forall x f, a <= x <= b -> Rnd_DN_pt F1 x f -> Rnd_DN_pt F2 x f.
Proof.
(* Goal: forall (F1 F2 : forall _ : R, Prop) (a b : R) (_ : F1 a) (_ : forall (x : R) (_ : and (Rle a x) (Rle x b)), iff (F1 x) (F2 x)) (x f : R) (_ : and (Rle a x) (Rle x b)) (_ : Rnd_DN_pt F1 x f), Rnd_DN_pt F2 x f *)
intros F1 F2 a b Ha HF x f Hx (H1, (H2, H3)).
(* Goal: round_pred (Rnd_NA_pt F) *)
split.
(* Goal: F2 f *)
(* Goal: and (Rle x f) (forall (g : R) (_ : F2 g) (_ : Rle x g), Rle f g) *)
apply -> HF.
(* Goal: F1 f *)
(* Goal: and (Rle a f) (Rle f b) *)
(* Goal: and (Rle x f) (forall (g : R) (_ : F2 g) (_ : Rle x g), Rle f g) *)
exact H1.
(* Goal: round_pred (Rnd_NA_pt F) *)
split.
(* Goal: Rle g f *)
now apply H3.
(* Goal: Rle f f2 *)
(* Goal: Rle (Rabs f2) (Rabs f) *)
now apply Rle_trans with (1 := H2).
(* Goal: round_pred (Rnd_NA_pt F) *)
split.
(* Goal: Rle f x *)
(* Goal: forall (g : R) (_ : F2 g) (_ : Rle g x), Rle g f *)
exact H2.
(* Goal: forall (g : R) (_ : F2 g) (_ : Rle x g), Rle f g *)
intros k Hk Hl.
(* Goal: Rle k f *)
destruct (Rlt_or_le k a) as [H|H].
(* Goal: Rle (Rabs (Rminus d x)) (Rabs (Rminus g x)) *)
(* Goal: Rle (Rabs (Rminus d x)) (Rabs (Rminus g x)) *)
(* Goal: or (P x d) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 d) *)
apply Rlt_le.
(* Goal: Rlt (Rabs (Rminus d x)) (Rabs (Rminus g x)) *)
(* Goal: Rle (Rabs (Rminus d x)) (Rabs (Rminus g x)) *)
(* Goal: or (P x d) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 d) *)
apply Rlt_le_trans with (1 := H).
(* Goal: Rle g f *)
now apply H3.
(* Goal: Rle g f *)
apply H3.
(* Goal: F1 k *)
(* Goal: Rle x k *)
(* Goal: Rle f k *)
apply <- HF.
(* Goal: F2 k *)
(* Goal: and (Rle a k) (Rle k b) *)
(* Goal: Rle x k *)
(* Goal: Rle f k *)
exact Hk.
(* Goal: round_pred (Rnd_NA_pt F) *)
split.
(* Goal: Rle k b *)
(* Goal: Rle x k *)
(* Goal: Rle f k *)
exact H.
(* Goal: Rle k b *)
(* Goal: Rle k x *)
now apply Rle_trans with (1 := Hl).
(* Goal: Rle x k *)
(* Goal: Rle f k *)
exact Hl.
Qed.

Theorem Rnd_UP_pt_equiv_format :
  forall F1 F2 : R -> Prop,
  forall a b : R,
  F1 b ->
  ( forall x, a <= x <= b -> (F1 x <-> F2 x) ) ->
  forall x f, a <= x <= b -> Rnd_UP_pt F1 x f -> Rnd_UP_pt F2 x f.
Proof.
(* Goal: forall (F1 F2 : forall _ : R, Prop) (a b : R) (_ : F1 b) (_ : forall (x : R) (_ : and (Rle a x) (Rle x b)), iff (F1 x) (F2 x)) (x f : R) (_ : and (Rle a x) (Rle x b)) (_ : Rnd_UP_pt F1 x f), Rnd_UP_pt F2 x f *)
intros F1 F2 a b Hb HF x f Hx (H1, (H2, H3)).
(* Goal: round_pred (Rnd_NA_pt F) *)
split.
(* Goal: F2 f *)
(* Goal: and (Rle x f) (forall (g : R) (_ : F2 g) (_ : Rle x g), Rle f g) *)
apply -> HF.
(* Goal: F1 f *)
(* Goal: and (Rle a f) (Rle f b) *)
(* Goal: and (Rle x f) (forall (g : R) (_ : F2 g) (_ : Rle x g), Rle f g) *)
exact H1.
(* Goal: round_pred (Rnd_NA_pt F) *)
split.
(* Goal: Rle f2 f *)
(* Goal: Rle f2 f *)
(* Goal: Rle (Rabs f2) (Rabs f) *)
(* Goal: iff (Rnd_NA_pt F x f) (Rnd_NG_pt F (fun x f : R => Rle (Rabs x) (Rabs f)) x f) *)
now apply Rle_trans with (2 := H2).
(* Goal: Rle g f *)
now apply H3.
(* Goal: round_pred (Rnd_NA_pt F) *)
split.
(* Goal: Rle f x *)
(* Goal: forall (g : R) (_ : F2 g) (_ : Rle g x), Rle g f *)
exact H2.
(* Goal: forall (g : R) (_ : F2 g) (_ : Rle x g), Rle f g *)
intros k Hk Hl.
(* Goal: Rle f k *)
destruct (Rle_or_lt k b) as [H|H].
(* Goal: Rle g f *)
apply H3.
(* Goal: F1 k *)
(* Goal: Rle x k *)
(* Goal: Rle f k *)
apply <- HF.
(* Goal: F2 k *)
(* Goal: and (Rle a k) (Rle k b) *)
(* Goal: Rle x k *)
(* Goal: Rle f k *)
exact Hk.
(* Goal: round_pred (Rnd_NA_pt F) *)
split.
(* Goal: Rle a k *)
(* Goal: Rle k b *)
(* Goal: Rle x k *)
(* Goal: Rle f k *)
now apply Rle_trans with (2 := Hl).
(* Goal: Rle k b *)
(* Goal: Rle x k *)
(* Goal: Rle f k *)
exact H.
(* Goal: Rle x k *)
(* Goal: Rle f k *)
exact Hl.
(* Goal: Rle (Rabs (Rminus d x)) (Rabs (Rminus g x)) *)
(* Goal: Rle (Rabs (Rminus d x)) (Rabs (Rminus g x)) *)
(* Goal: or (P x d) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 d) *)
apply Rlt_le.
(* Goal: Rlt f k *)
apply Rle_lt_trans with (2 := H).
(* Goal: Rle g f *)
now apply H3.
Qed.

(** ensures a real number can always be rounded *)
Inductive satisfies_any (F : R -> Prop) :=
  Satisfies_any :
    F 0 -> ( forall x : R, F x -> F (-x) ) ->
    round_pred_total (Rnd_DN_pt F) -> satisfies_any F.

Theorem satisfies_any_eq :
  forall F1 F2 : R -> Prop,
  ( forall x, F1 x <-> F2 x ) ->
  satisfies_any F1 ->
  satisfies_any F2.
Proof.
(* Goal: forall (F1 F2 : forall _ : R, Prop) (_ : forall x : R, iff (F1 x) (F2 x)) (_ : satisfies_any F1), satisfies_any F2 *)
intros F1 F2 Heq (Hzero, Hsym, Hrnd).
(* Goal: round_pred (Rnd_NA_pt F) *)
split.
(* Goal: F2 f *)
(* Goal: and (Rle f x) (forall (g : R) (_ : F2 g) (_ : Rle g x), Rle g f) *)
now apply -> Heq.
(* Goal: forall (x : R) (_ : F2 x), F2 (Ropp x) *)
(* Goal: round_pred_total (Rnd_DN_pt F2) *)
intros x Hx.
(* Goal: F2 (Ropp x) *)
(* Goal: round_pred_total (Rnd_DN_pt F2) *)
apply -> Heq.
(* Goal: F1 (Ropp x) *)
(* Goal: round_pred_total (Rnd_DN_pt F2) *)
apply Hsym.
(* Goal: F1 g *)
(* Goal: Rle g x *)
now apply <- Heq.
(* Goal: round_pred_total (Rnd_NA_pt F) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
intros x.
(* Goal: @ex R (fun f : R => Rnd_DN_pt F2 x f) *)
destruct (Hrnd x) as (f, (H1, (H2, H3))).
(* Goal: @ex R (fun f : R => Rnd_NA_pt F x f) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
exists f.
(* Goal: round_pred (Rnd_NA_pt F) *)
split.
(* Goal: F2 f *)
(* Goal: and (Rle f x) (forall (g : R) (_ : F2 g) (_ : Rle g x), Rle g f) *)
now apply -> Heq.
(* Goal: round_pred (Rnd_NA_pt F) *)
split.
(* Goal: Rle f x *)
(* Goal: forall (g : R) (_ : F2 g) (_ : Rle g x), Rle g f *)
exact H2.
(* Goal: forall (g : R) (_ : F2 g) (_ : Rle g x), Rle g f *)
intros g Hg Hgx.
(* Goal: Rle g f *)
apply H3.
(* Goal: F1 g *)
(* Goal: Rle g x *)
now apply <- Heq.
(* Goal: Rle g x *)
exact Hgx.
Qed.

Theorem satisfies_any_imp_DN :
  forall F : R -> Prop,
  satisfies_any F ->
  round_pred (Rnd_DN_pt F).
Proof.
(* Goal: forall (F : forall _ : R, Prop) (_ : satisfies_any F), round_pred (Rnd_DN_pt F) *)
intros F (_,_,Hrnd).
(* Goal: round_pred (Rnd_NA_pt F) *)
split.
(* Goal: round_pred_total (Rnd_DN_pt F) *)
(* Goal: round_pred_monotone (Rnd_DN_pt F) *)
apply Hrnd.
(* Goal: round_pred_monotone (Rnd_DN_pt F) *)
apply Rnd_DN_pt_monotone.
Qed.

Theorem satisfies_any_imp_UP :
  forall F : R -> Prop,
  satisfies_any F ->
  round_pred (Rnd_UP_pt F).
Proof.
(* Goal: forall (F : forall _ : R, Prop) (_ : satisfies_any F), round_pred (Rnd_NA_pt F) *)
intros F Hany.
(* Goal: round_pred (Rnd_NA_pt F) *)
split.
(* Goal: round_pred_total (Rnd_NA_pt F) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
intros x.
(* Goal: @ex R (fun f : R => Rnd_UP_pt F x f) *)
(* Goal: round_pred_monotone (Rnd_UP_pt F) *)
destruct (proj1 (satisfies_any_imp_DN F Hany) (-x)) as (f, Hf).
(* Goal: @ex R (fun f : R => Rnd_UP_pt F x f) *)
(* Goal: round_pred_monotone (Rnd_UP_pt F) *)
exists (-f).
(* Goal: Rnd_UP_pt F x (Ropp f) *)
(* Goal: round_pred_monotone (Rnd_UP_pt F) *)
rewrite <- (Ropp_involutive x).
(* Goal: Rnd_UP_pt F (Ropp (Ropp x)) (Ropp f) *)
(* Goal: round_pred_monotone (Rnd_UP_pt F) *)
apply Rnd_DN_UP_pt_sym.
(* Goal: F (IZR Z0) *)
apply Hany.
(* Goal: Rnd_DN_pt F (Ropp x) f *)
(* Goal: round_pred_monotone (Rnd_UP_pt F) *)
exact Hf.
(* Goal: round_pred_monotone (Rnd_UP_pt F) *)
apply Rnd_UP_pt_monotone.
Qed.

Theorem satisfies_any_imp_ZR :
  forall F : R -> Prop,
  satisfies_any F ->
  round_pred (Rnd_ZR_pt F).
Proof.
(* Goal: forall (F : forall _ : R, Prop) (_ : satisfies_any F), round_pred (Rnd_NA_pt F) *)
intros F Hany.
(* Goal: round_pred (Rnd_NA_pt F) *)
split.
(* Goal: round_pred_total (Rnd_NA_pt F) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
intros x.
(* Goal: @ex R (fun f : R => Rnd_ZR_pt F x f) *)
(* Goal: round_pred_monotone (Rnd_ZR_pt F) *)
destruct (Rle_or_lt 0 x) as [Hx|Hx].
(* positive *)
(* Goal: @ex R (fun f : R => Rnd_ZR_pt F x f) *)
(* Goal: @ex R (fun f : R => Rnd_ZR_pt F x f) *)
(* Goal: round_pred_monotone (Rnd_ZR_pt F) *)
destruct (proj1 (satisfies_any_imp_DN F Hany) x) as (f, Hf).
(* Goal: @ex R (fun f : R => Rnd_NA_pt F x f) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
exists f.
(* Goal: round_pred (Rnd_NA_pt F) *)
split.
(* Goal: forall _ : Rle x (IZR Z0), Rnd_UP_pt F x f *)
(* Goal: round_pred_monotone (Rnd_ZR_pt F) *)
now intros _.
(* Goal: forall _ : Rle (IZR Z0) x, Rnd_DN_pt F x f *)
(* Goal: forall _ : Rle x (IZR Z0), Rnd_UP_pt F x f *)
(* Goal: round_pred_monotone (Rnd_ZR_pt F) *)
intros Hx'.
(* zero *)
(* Goal: Rnd_UP_pt F x f *)
(* Goal: @ex R (fun f : R => Rnd_ZR_pt F x f) *)
(* Goal: round_pred_monotone (Rnd_ZR_pt F) *)
assert (x = 0).
(* Goal: @eq R (Rabs (Rminus f x)) (Rabs (Rminus g x)) *)
(* Goal: Rle (Rabs g) (Rabs f) *)
(* Goal: Rle (Rabs g) (Rabs f) *)
now apply Rle_antisym.
(* Goal: Rnd_UP_pt F x f *)
(* Goal: @ex R (fun f : R => Rnd_ZR_pt F x f) *)
(* Goal: round_pred_monotone (Rnd_ZR_pt F) *)
rewrite H in Hf |- *.
(* Goal: Rnd_UP_pt F (IZR Z0) f *)
(* Goal: @ex R (fun f : R => Rnd_ZR_pt F x f) *)
(* Goal: round_pred_monotone (Rnd_ZR_pt F) *)
clear H Hx Hx'.
(* Goal: Rnd_UP_pt F (IZR Z0) f *)
(* Goal: @ex R (fun f : R => Rnd_ZR_pt F x f) *)
(* Goal: round_pred_monotone (Rnd_ZR_pt F) *)
rewrite Rnd_DN_pt_idempotent with (1 := Hf).
(* Goal: Rnd_UP_pt F (IZR Z0) (IZR Z0) *)
(* Goal: F (IZR Z0) *)
(* Goal: @ex R (fun f : R => Rnd_ZR_pt F x f) *)
(* Goal: round_pred_monotone (Rnd_ZR_pt F) *)
apply Rnd_UP_pt_refl.
(* Goal: F (IZR Z0) *)
apply Hany.
(* Goal: F (IZR Z0) *)
apply Hany.
(* negative *)
(* Goal: @ex R (fun f : R => Rnd_ZR_pt F x f) *)
(* Goal: round_pred_monotone (Rnd_ZR_pt F) *)
destruct (proj1 (satisfies_any_imp_UP F Hany) x) as (f, Hf).
(* Goal: @ex R (fun f : R => Rnd_NA_pt F x f) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
exists f.
(* Goal: round_pred (Rnd_NA_pt F) *)
split.
(* Goal: forall _ : Rle (IZR Z0) x, Rnd_DN_pt F x f *)
(* Goal: forall _ : Rle x (IZR Z0), Rnd_UP_pt F x f *)
(* Goal: round_pred_monotone (Rnd_ZR_pt F) *)
intros Hx'.
(* Goal: Rnd_DN_pt F x f *)
(* Goal: forall _ : Rle x (IZR Z0), Rnd_UP_pt F x f *)
(* Goal: round_pred_monotone (Rnd_ZR_pt F) *)
elim (Rlt_irrefl 0).
(* Goal: Rlt (IZR Z0) (IZR Z0) *)
(* Goal: forall _ : Rle x (IZR Z0), Rnd_UP_pt F x f *)
(* Goal: round_pred_monotone (Rnd_ZR_pt F) *)
now apply Rle_lt_trans with x.
(* Goal: forall _ : Rle x (IZR Z0), Rnd_UP_pt F x f *)
(* Goal: round_pred_monotone (Rnd_ZR_pt F) *)
now intros _.
(* . *)
(* Goal: round_pred_monotone (Rnd_ZR_pt F) *)
apply Rnd_ZR_pt_monotone.
(* Goal: F (IZR Z0) *)
apply Hany.
Qed.

Definition NG_existence_prop (F : R -> Prop) (P : R -> R -> Prop) :=
  forall x d u, ~F x -> Rnd_DN_pt F x d -> Rnd_UP_pt F x u -> P x u \/ P x d.

Theorem satisfies_any_imp_NG :
  forall (F : R -> Prop) (P : R -> R -> Prop),
  satisfies_any F ->
  NG_existence_prop F P ->
  round_pred_total (Rnd_NG_pt F P).
Proof.
(* Goal: forall (F : forall _ : R, Prop) (P : forall (_ : R) (_ : R), Prop) (_ : satisfies_any F) (_ : NG_existence_prop F P), round_pred_total (Rnd_NG_pt F P) *)
intros F P Hany HP x.
(* Goal: @ex R (fun f : R => Rnd_NG_pt F P x f) *)
destruct (proj1 (satisfies_any_imp_DN F Hany) x) as (d, Hd).
(* Goal: @ex R (fun f : R => Rnd_NG_pt F P x f) *)
destruct (proj1 (satisfies_any_imp_UP F Hany) x) as (u, Hu).
(* Goal: @ex R (fun f : R => Rnd_NG_pt F P x f) *)
destruct (total_order_T (Rabs (u - x)) (Rabs (d - x))) as [[H|H]|H].
(* |up(x) - x| < |dn(x) - x| *)
(* Goal: @ex R (fun f : R => Rnd_NG_pt F P x f) *)
(* Goal: @ex R (fun f : R => Rnd_NG_pt F P x f) *)
(* Goal: @ex R (fun f : R => Rnd_NG_pt F P x f) *)
exists u.
(* Goal: round_pred (Rnd_NA_pt F) *)
split.
(* - . *)
(* Goal: round_pred (Rnd_NA_pt F) *)
split.
(* Goal: Rle x u *)
(* Goal: or (Rle (Rabs x) (Rabs u)) (Rle (Rabs x) (Rabs d)) *)
(* Goal: round_pred_total (Rnd_NA_pt F) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
apply Hu.
(* Goal: forall (g : R) (_ : F g), Rle (Rabs (Rminus d x)) (Rabs (Rminus g x)) *)
(* Goal: or (P x d) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 d) *)
intros g Hg.
(* Goal: Rle (Rabs (Rminus d x)) (Rabs (Rminus g x)) *)
(* Goal: or (P x d) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 d) *)
destruct (Rle_or_lt x g) as [Hxg|Hxg].
(* Goal: Rle (Rabs (Rminus u x)) (Rabs (Rminus g x)) *)
(* Goal: Rle (Rabs (Rminus d x)) (Rabs (Rminus g x)) *)
(* Goal: or (P x d) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 d) *)
rewrite 2!Rabs_pos_eq.
(* Goal: Rle (Rminus g x) (Rminus d x) *)
(* Goal: Rle (Rminus g x) (IZR Z0) *)
(* Goal: Rle (Rminus d x) (IZR Z0) *)
(* Goal: or (P x d) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 d) *)
apply Rplus_le_compat_r.
(* Goal: Rle u g *)
(* Goal: Rle (IZR Z0) (Rminus g x) *)
(* Goal: Rle (IZR Z0) (Rminus u x) *)
(* Goal: Rle (Rabs (Rminus d x)) (Rabs (Rminus g x)) *)
(* Goal: or (P x d) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 d) *)
now apply Hu.
(* Goal: Rle (IZR Z0) (Rminus g x) *)
(* Goal: Rle (IZR Z0) (Rminus u x) *)
(* Goal: Rle (Rabs (Rminus d x)) (Rabs (Rminus g x)) *)
(* Goal: or (P x d) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 d) *)
now apply Rle_0_minus.
(* Goal: Rle (IZR Z0) (Rminus u x) *)
(* Goal: Rle (Rabs (Rminus d x)) (Rabs (Rminus g x)) *)
(* Goal: or (P x d) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 d) *)
apply Rle_0_minus.
(* Goal: Rle x u *)
(* Goal: or (Rle (Rabs x) (Rabs u)) (Rle (Rabs x) (Rabs d)) *)
(* Goal: round_pred_total (Rnd_NA_pt F) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
apply Hu.
(* Goal: Rle (Rabs (Rminus d x)) (Rabs (Rminus g x)) *)
(* Goal: or (P x d) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 d) *)
apply Rlt_le in Hxg.
(* Goal: Rle (Rabs (Rminus d x)) (Rabs (Rminus g x)) *)
(* Goal: Rle (Rabs (Rminus d x)) (Rabs (Rminus g x)) *)
(* Goal: or (P x d) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 d) *)
apply Rlt_le.
(* Goal: Rlt (Rabs (Rminus d x)) (Rabs (Rminus g x)) *)
(* Goal: Rle (Rabs (Rminus d x)) (Rabs (Rminus g x)) *)
(* Goal: or (P x d) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 d) *)
apply Rlt_le_trans with (1 := H).
(* Goal: Rle (Rabs (Rminus d x)) (Rabs (Rminus g x)) *)
(* Goal: or (P x u) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 u) *)
(* Goal: @ex R (fun f : R => Rnd_NG_pt F P x f) *)
(* Goal: @ex R (fun f : R => Rnd_NG_pt F P x f) *)
do 2 rewrite <- (Rabs_minus_sym x).
(* Goal: Rle (Rabs (Rminus u x)) (Rabs (Rminus g x)) *)
(* Goal: Rle (Rabs (Rminus d x)) (Rabs (Rminus g x)) *)
(* Goal: or (P x d) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 d) *)
rewrite 2!Rabs_pos_eq.
(* Goal: Rle (Rminus x d) (Rminus x g) *)
(* Goal: Rle (IZR Z0) (Rminus x g) *)
(* Goal: Rle (IZR Z0) (Rminus x d) *)
(* Goal: or (P x u) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 u) *)
(* Goal: @ex R (fun f : R => Rnd_NG_pt F P x f) *)
(* Goal: @ex R (fun f : R => Rnd_NG_pt F P x f) *)
apply Rplus_le_compat_l.
(* Goal: Rle (Ropp x) (Ropp d) *)
(* Goal: Rle d (IZR Z0) *)
(* Goal: round_pred_total (Rnd_NA_pt F) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
apply Ropp_le_contravar.
(* Goal: Rle g d *)
(* Goal: Rle (Rminus g x) (IZR Z0) *)
(* Goal: Rle (Rminus d x) (IZR Z0) *)
(* Goal: or (P x d) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 d) *)
now apply Hd.
(* Goal: Rle (IZR Z0) (Rminus g x) *)
(* Goal: Rle (IZR Z0) (Rminus u x) *)
(* Goal: Rle (Rabs (Rminus d x)) (Rabs (Rminus g x)) *)
(* Goal: or (P x d) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 d) *)
now apply Rle_0_minus.
(* Goal: Rle (IZR Z0) (Rminus u x) *)
(* Goal: Rle (Rabs (Rminus d x)) (Rabs (Rminus g x)) *)
(* Goal: or (P x d) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 d) *)
apply Rle_0_minus.
(* Goal: Rle d x *)
(* Goal: round_pred_total (Rnd_NA_pt F) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
apply Hd.
(* - . *)
(* Goal: or (Rle (Rabs x) (Rabs u)) (Rle (Rabs x) (Rabs d)) *)
(* Goal: round_pred_total (Rnd_NA_pt F) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
right.
(* Goal: forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 d *)
intros f Hf.
(* Goal: @eq R f d *)
destruct (Rnd_N_pt_DN_or_UP_eq F x _ _ _ Hd Hu Hf) as [K|K] ; rewrite K.
(* Goal: @eq R u d *)
elim Rlt_not_le with (1 := H).
(* Goal: Rle (Rabs (Rminus u x)) (Rabs (Rminus d x)) *)
rewrite <- K.
(* Goal: Rnd_NG_pt F (fun x f : R => Rle (Rabs x) (Rabs f)) x f *)
(* Goal: F (IZR Z0) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
apply Hf.
(* Goal: Rle x u *)
(* Goal: or (Rle (Rabs x) (Rabs u)) (Rle (Rabs x) (Rabs d)) *)
(* Goal: round_pred_total (Rnd_NA_pt F) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
apply Hu.
(* Goal: @eq R d d *)
(* Goal: @eq R u d *)
apply refl_equal.
(* |up(x) - x| = |dn(x) - x| *)
(* Goal: @ex R (fun f : R => Rnd_NG_pt F P x f) *)
(* Goal: @ex R (fun f : R => Rnd_NG_pt F P x f) *)
destruct (Req_dec x d) as [He|Hne].
(* - x = d = u *)
(* Goal: @ex R (fun f : R => Rnd_NG_pt F P x f) *)
(* Goal: @ex R (fun f : R => Rnd_NG_pt F P x f) *)
(* Goal: @ex R (fun f : R => Rnd_NG_pt F P x f) *)
exists x.
(* Goal: round_pred (Rnd_NA_pt F) *)
split.
(* Goal: Rnd_N_pt F x x *)
(* Goal: or (P x x) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 x) *)
(* Goal: @ex R (fun f : R => Rnd_NG_pt F P x f) *)
(* Goal: @ex R (fun f : R => Rnd_NG_pt F P x f) *)
apply Rnd_N_pt_refl.
(* Goal: F x *)
(* Goal: @ex R (fun f : R => Rnd_NG_pt F P x f) *)
(* Goal: @ex R (fun f : R => Rnd_NG_pt F P x f) *)
rewrite He.
(* Goal: Rle d x *)
(* Goal: round_pred_total (Rnd_NA_pt F) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
apply Hd.
(* Goal: or (Rle (Rabs x) (Rabs u)) (Rle (Rabs x) (Rabs d)) *)
(* Goal: round_pred_total (Rnd_NA_pt F) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
right.
(* Goal: forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 x *)
(* Goal: @ex R (fun f : R => Rnd_NG_pt F P x f) *)
(* Goal: @ex R (fun f : R => Rnd_NG_pt F P x f) *)
intros.
(* Goal: @eq R f2 x *)
(* Goal: @ex R (fun f : R => Rnd_NG_pt F P x f) *)
(* Goal: @ex R (fun f : R => Rnd_NG_pt F P x f) *)
apply Rnd_N_pt_idempotent with (1 := H0).
(* Goal: F x *)
(* Goal: @ex R (fun f : R => Rnd_NG_pt F P x f) *)
(* Goal: @ex R (fun f : R => Rnd_NG_pt F P x f) *)
rewrite He.
(* Goal: Rle d x *)
(* Goal: round_pred_total (Rnd_NA_pt F) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
apply Hd.
(* Goal: @ex R (fun f : R => Rnd_NG_pt F P x f) *)
(* Goal: @ex R (fun f : R => Rnd_NG_pt F P x f) *)
assert (Hf : ~F x).
(* Goal: not (F x) *)
(* Goal: @ex R (fun f : R => Rnd_NG_pt F P x f) *)
(* Goal: @ex R (fun f : R => Rnd_NG_pt F P x f) *)
intros Hf.
(* Goal: False *)
(* Goal: @ex R (fun f : R => Rnd_NG_pt F P x f) *)
(* Goal: @ex R (fun f : R => Rnd_NG_pt F P x f) *)
apply Hne.
(* Goal: @eq R x d *)
(* Goal: @ex R (fun f : R => Rnd_NG_pt F P x f) *)
(* Goal: @ex R (fun f : R => Rnd_NG_pt F P x f) *)
apply sym_eq.
(* Goal: @eq R d x *)
(* Goal: @ex R (fun f : R => Rnd_NG_pt F P x f) *)
(* Goal: @ex R (fun f : R => Rnd_NG_pt F P x f) *)
now apply Rnd_DN_pt_idempotent with (1 := Hd).
(* Goal: @ex R (fun f : R => Rnd_NG_pt F P x f) *)
(* Goal: @ex R (fun f : R => Rnd_NG_pt F P x f) *)
destruct (HP x _ _ Hf Hd Hu) as [H'|H'].
(* - u >> d *)
(* Goal: @ex R (fun f : R => Rnd_NG_pt F P x f) *)
(* Goal: @ex R (fun f : R => Rnd_NG_pt F P x f) *)
(* Goal: @ex R (fun f : R => Rnd_NG_pt F P x f) *)
exists u.
(* Goal: round_pred (Rnd_NA_pt F) *)
split.
(* Goal: round_pred (Rnd_NA_pt F) *)
split.
(* Goal: Rle x u *)
(* Goal: or (Rle (Rabs x) (Rabs u)) (Rle (Rabs x) (Rabs d)) *)
(* Goal: round_pred_total (Rnd_NA_pt F) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
apply Hu.
(* Goal: forall (g : R) (_ : F g), Rle (Rabs (Rminus d x)) (Rabs (Rminus g x)) *)
(* Goal: or (P x d) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 d) *)
intros g Hg.
(* Goal: Rle (Rabs (Rminus d x)) (Rabs (Rminus g x)) *)
(* Goal: or (P x d) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 d) *)
destruct (Rle_or_lt x g) as [Hxg|Hxg].
(* Goal: Rle (Rabs (Rminus u x)) (Rabs (Rminus g x)) *)
(* Goal: Rle (Rabs (Rminus d x)) (Rabs (Rminus g x)) *)
(* Goal: or (P x d) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 d) *)
rewrite 2!Rabs_pos_eq.
(* Goal: Rle (Rminus g x) (Rminus d x) *)
(* Goal: Rle (Rminus g x) (IZR Z0) *)
(* Goal: Rle (Rminus d x) (IZR Z0) *)
(* Goal: or (P x d) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 d) *)
apply Rplus_le_compat_r.
(* Goal: Rle u g *)
(* Goal: Rle (IZR Z0) (Rminus g x) *)
(* Goal: Rle (IZR Z0) (Rminus u x) *)
(* Goal: Rle (Rabs (Rminus d x)) (Rabs (Rminus g x)) *)
(* Goal: or (P x d) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 d) *)
now apply Hu.
(* Goal: Rle (IZR Z0) (Rminus g x) *)
(* Goal: Rle (IZR Z0) (Rminus u x) *)
(* Goal: Rle (Rabs (Rminus d x)) (Rabs (Rminus g x)) *)
(* Goal: or (P x d) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 d) *)
now apply Rle_0_minus.
(* Goal: Rle (IZR Z0) (Rminus u x) *)
(* Goal: Rle (Rabs (Rminus d x)) (Rabs (Rminus g x)) *)
(* Goal: or (P x d) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 d) *)
apply Rle_0_minus.
(* Goal: Rle x u *)
(* Goal: or (Rle (Rabs x) (Rabs u)) (Rle (Rabs x) (Rabs d)) *)
(* Goal: round_pred_total (Rnd_NA_pt F) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
apply Hu.
(* Goal: Rle (Rabs (Rminus d x)) (Rabs (Rminus g x)) *)
(* Goal: or (P x d) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 d) *)
apply Rlt_le in Hxg.
(* Goal: Rle (Rabs (Rminus u x)) (Rabs (Rminus g x)) *)
(* Goal: or (P x u) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 u) *)
(* Goal: @ex R (fun f : R => Rnd_NG_pt F P x f) *)
(* Goal: @ex R (fun f : R => Rnd_NG_pt F P x f) *)
rewrite H.
(* Goal: Rle (Rabs (Rminus d x)) (Rabs (Rminus g x)) *)
(* Goal: or (P x d) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 d) *)
rewrite 2!Rabs_left1.
(* Goal: Rle (Ropp x) (Ropp d) *)
(* Goal: Rle d (IZR Z0) *)
(* Goal: round_pred_total (Rnd_NA_pt F) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
apply Ropp_le_contravar.
(* Goal: Rle (Rminus g x) (Rminus d x) *)
(* Goal: Rle (Rminus g x) (IZR Z0) *)
(* Goal: Rle (Rminus d x) (IZR Z0) *)
(* Goal: or (P x d) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 d) *)
apply Rplus_le_compat_r.
(* Goal: Rle g d *)
(* Goal: Rle (Rminus g x) (IZR Z0) *)
(* Goal: Rle (Rminus d x) (IZR Z0) *)
(* Goal: or (P x d) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 d) *)
now apply Hd.
(* Goal: Rle (Rminus g x) (IZR Z0) *)
(* Goal: Rle (Rminus d x) (IZR Z0) *)
(* Goal: or (P x d) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 d) *)
now apply Rle_minus.
(* Goal: Rle (Rminus d x) (IZR Z0) *)
(* Goal: or (P x d) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 d) *)
apply Rle_minus.
(* Goal: Rle d x *)
(* Goal: round_pred_total (Rnd_NA_pt F) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
apply Hd.
(* Goal: or (Rle (Rabs x) (Rabs u)) (Rle (Rabs x) (Rabs d)) *)
(* Goal: or (Rle (Rabs x) (Rabs u)) (Rle (Rabs x) (Rabs d)) *)
(* Goal: round_pred_total (Rnd_NA_pt F) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
now left.
(* - d >> u *)
(* Goal: @ex R (fun f : R => Rnd_NG_pt F P x f) *)
exists d.
(* Goal: round_pred (Rnd_NA_pt F) *)
split.
(* Goal: round_pred (Rnd_NA_pt F) *)
split.
(* Goal: Rle d x *)
(* Goal: round_pred_total (Rnd_NA_pt F) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
apply Hd.
(* Goal: forall (g : R) (_ : F g), Rle (Rabs (Rminus d x)) (Rabs (Rminus g x)) *)
(* Goal: or (P x d) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 d) *)
intros g Hg.
(* Goal: Rle (Rabs (Rminus d x)) (Rabs (Rminus g x)) *)
(* Goal: or (P x d) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 d) *)
destruct (Rle_or_lt x g) as [Hxg|Hxg].
(* Goal: Rle (Rabs (Rminus d x)) (Rabs (Rminus g x)) *)
(* Goal: Rle (Rabs (Rminus d x)) (Rabs (Rminus g x)) *)
(* Goal: or (P x d) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 d) *)
(* Goal: @ex R (fun f : R => Rnd_NG_pt F P x f) *)
rewrite <- H.
(* Goal: Rle (Rabs (Rminus u x)) (Rabs (Rminus g x)) *)
(* Goal: Rle (Rabs (Rminus d x)) (Rabs (Rminus g x)) *)
(* Goal: or (P x d) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 d) *)
rewrite 2!Rabs_pos_eq.
(* Goal: Rle (Rminus g x) (Rminus d x) *)
(* Goal: Rle (Rminus g x) (IZR Z0) *)
(* Goal: Rle (Rminus d x) (IZR Z0) *)
(* Goal: or (P x d) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 d) *)
apply Rplus_le_compat_r.
(* Goal: Rle u g *)
(* Goal: Rle (IZR Z0) (Rminus g x) *)
(* Goal: Rle (IZR Z0) (Rminus u x) *)
(* Goal: Rle (Rabs (Rminus d x)) (Rabs (Rminus g x)) *)
(* Goal: or (P x d) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 d) *)
now apply Hu.
(* Goal: Rle (IZR Z0) (Rminus g x) *)
(* Goal: Rle (IZR Z0) (Rminus u x) *)
(* Goal: Rle (Rabs (Rminus d x)) (Rabs (Rminus g x)) *)
(* Goal: or (P x d) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 d) *)
now apply Rle_0_minus.
(* Goal: Rle (IZR Z0) (Rminus u x) *)
(* Goal: Rle (Rabs (Rminus d x)) (Rabs (Rminus g x)) *)
(* Goal: or (P x d) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 d) *)
apply Rle_0_minus.
(* Goal: Rle x u *)
(* Goal: or (Rle (Rabs x) (Rabs u)) (Rle (Rabs x) (Rabs d)) *)
(* Goal: round_pred_total (Rnd_NA_pt F) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
apply Hu.
(* Goal: Rle (Rabs (Rminus d x)) (Rabs (Rminus g x)) *)
(* Goal: or (P x d) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 d) *)
apply Rlt_le in Hxg.
(* Goal: Rle (Rabs (Rminus d x)) (Rabs (Rminus g x)) *)
(* Goal: or (P x d) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 d) *)
rewrite 2!Rabs_left1.
(* Goal: Rle (Ropp x) (Ropp d) *)
(* Goal: Rle d (IZR Z0) *)
(* Goal: round_pred_total (Rnd_NA_pt F) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
apply Ropp_le_contravar.
(* Goal: Rle (Rminus g x) (Rminus d x) *)
(* Goal: Rle (Rminus g x) (IZR Z0) *)
(* Goal: Rle (Rminus d x) (IZR Z0) *)
(* Goal: or (P x d) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 d) *)
apply Rplus_le_compat_r.
(* Goal: Rle g d *)
(* Goal: Rle (Rminus g x) (IZR Z0) *)
(* Goal: Rle (Rminus d x) (IZR Z0) *)
(* Goal: or (P x d) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 d) *)
now apply Hd.
(* Goal: Rle (Rminus g x) (IZR Z0) *)
(* Goal: Rle (Rminus d x) (IZR Z0) *)
(* Goal: or (P x d) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 d) *)
now apply Rle_minus.
(* Goal: Rle (Rminus d x) (IZR Z0) *)
(* Goal: or (P x d) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 d) *)
apply Rle_minus.
(* Goal: Rle d x *)
(* Goal: round_pred_total (Rnd_NA_pt F) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
apply Hd.
(* Goal: or (Rle (Rabs x) (Rabs u)) (Rle (Rabs x) (Rabs d)) *)
(* Goal: or (Rle (Rabs x) (Rabs u)) (Rle (Rabs x) (Rabs d)) *)
(* Goal: round_pred_total (Rnd_NA_pt F) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
now left.
(* |up(x) - x| > |dn(x) - x| *)
(* Goal: @ex R (fun f : R => Rnd_NG_pt F P x f) *)
exists d.
(* Goal: round_pred (Rnd_NA_pt F) *)
split.
(* Goal: round_pred (Rnd_NA_pt F) *)
split.
(* Goal: Rle d x *)
(* Goal: round_pred_total (Rnd_NA_pt F) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
apply Hd.
(* Goal: forall (g : R) (_ : F g), Rle (Rabs (Rminus d x)) (Rabs (Rminus g x)) *)
(* Goal: or (P x d) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 d) *)
intros g Hg.
(* Goal: Rle (Rabs (Rminus d x)) (Rabs (Rminus g x)) *)
(* Goal: or (P x d) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 d) *)
destruct (Rle_or_lt x g) as [Hxg|Hxg].
(* Goal: Rle (Rabs (Rminus d x)) (Rabs (Rminus g x)) *)
(* Goal: Rle (Rabs (Rminus d x)) (Rabs (Rminus g x)) *)
(* Goal: or (P x d) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 d) *)
apply Rlt_le.
(* Goal: Rlt (Rabs (Rminus d x)) (Rabs (Rminus g x)) *)
(* Goal: Rle (Rabs (Rminus d x)) (Rabs (Rminus g x)) *)
(* Goal: or (P x d) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 d) *)
apply Rlt_le_trans with (1 := H).
(* Goal: Rle (Rabs (Rminus u x)) (Rabs (Rminus g x)) *)
(* Goal: Rle (Rabs (Rminus d x)) (Rabs (Rminus g x)) *)
(* Goal: or (P x d) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 d) *)
rewrite 2!Rabs_pos_eq.
(* Goal: Rle (Rminus g x) (Rminus d x) *)
(* Goal: Rle (Rminus g x) (IZR Z0) *)
(* Goal: Rle (Rminus d x) (IZR Z0) *)
(* Goal: or (P x d) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 d) *)
apply Rplus_le_compat_r.
(* Goal: Rle u g *)
(* Goal: Rle (IZR Z0) (Rminus g x) *)
(* Goal: Rle (IZR Z0) (Rminus u x) *)
(* Goal: Rle (Rabs (Rminus d x)) (Rabs (Rminus g x)) *)
(* Goal: or (P x d) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 d) *)
now apply Hu.
(* Goal: Rle (IZR Z0) (Rminus g x) *)
(* Goal: Rle (IZR Z0) (Rminus u x) *)
(* Goal: Rle (Rabs (Rminus d x)) (Rabs (Rminus g x)) *)
(* Goal: or (P x d) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 d) *)
now apply Rle_0_minus.
(* Goal: Rle (IZR Z0) (Rminus u x) *)
(* Goal: Rle (Rabs (Rminus d x)) (Rabs (Rminus g x)) *)
(* Goal: or (P x d) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 d) *)
apply Rle_0_minus.
(* Goal: Rle x u *)
(* Goal: or (Rle (Rabs x) (Rabs u)) (Rle (Rabs x) (Rabs d)) *)
(* Goal: round_pred_total (Rnd_NA_pt F) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
apply Hu.
(* Goal: Rle (Rabs (Rminus d x)) (Rabs (Rminus g x)) *)
(* Goal: or (P x d) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 d) *)
apply Rlt_le in Hxg.
(* Goal: Rle (Rabs (Rminus d x)) (Rabs (Rminus g x)) *)
(* Goal: or (P x d) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 d) *)
rewrite 2!Rabs_left1.
(* Goal: Rle (Ropp x) (Ropp d) *)
(* Goal: Rle d (IZR Z0) *)
(* Goal: round_pred_total (Rnd_NA_pt F) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
apply Ropp_le_contravar.
(* Goal: Rle (Rminus g x) (Rminus d x) *)
(* Goal: Rle (Rminus g x) (IZR Z0) *)
(* Goal: Rle (Rminus d x) (IZR Z0) *)
(* Goal: or (P x d) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 d) *)
apply Rplus_le_compat_r.
(* Goal: Rle g d *)
(* Goal: Rle (Rminus g x) (IZR Z0) *)
(* Goal: Rle (Rminus d x) (IZR Z0) *)
(* Goal: or (P x d) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 d) *)
now apply Hd.
(* Goal: Rle (Rminus g x) (IZR Z0) *)
(* Goal: Rle (Rminus d x) (IZR Z0) *)
(* Goal: or (P x d) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 d) *)
now apply Rle_minus.
(* Goal: Rle (Rminus d x) (IZR Z0) *)
(* Goal: or (P x d) (forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 d) *)
apply Rle_minus.
(* Goal: Rle d x *)
(* Goal: round_pred_total (Rnd_NA_pt F) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
apply Hd.
(* Goal: or (Rle (Rabs x) (Rabs u)) (Rle (Rabs x) (Rabs d)) *)
(* Goal: round_pred_total (Rnd_NA_pt F) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
right.
(* Goal: forall (f2 : R) (_ : Rnd_N_pt F x f2), @eq R f2 d *)
intros f Hf.
(* Goal: @eq R f d *)
destruct (Rnd_N_pt_DN_or_UP_eq F x _ _ _ Hd Hu Hf) as [K|K] ; rewrite K.
(* Goal: @eq R d d *)
(* Goal: @eq R u d *)
apply refl_equal.
(* Goal: @eq R u d *)
elim Rlt_not_le with (1 := H).
(* Goal: Rle (Rabs (Rminus u x)) (Rabs (Rminus d x)) *)
rewrite <- K.
(* Goal: Rnd_NG_pt F (fun x f : R => Rle (Rabs x) (Rabs f)) x f *)
(* Goal: F (IZR Z0) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
apply Hf.
(* Goal: Rle d x *)
(* Goal: round_pred_total (Rnd_NA_pt F) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
apply Hd.
Qed.

Theorem satisfies_any_imp_NA :
  forall F : R -> Prop,
  satisfies_any F ->
  round_pred (Rnd_NA_pt F).
Proof.
(* Goal: forall (F : forall _ : R, Prop) (_ : satisfies_any F), round_pred (Rnd_NA_pt F) *)
intros F Hany.
(* Goal: round_pred (Rnd_NA_pt F) *)
split.
(* Goal: round_pred_total (Rnd_NA_pt F) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
assert (H : round_pred_total (Rnd_NG_pt F (fun a b => (Rabs a <= Rabs b)%R))).
(* Goal: round_pred_total (Rnd_NG_pt F (fun a b : R => Rle (Rabs a) (Rabs b))) *)
(* Goal: round_pred_total (Rnd_NA_pt F) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
apply satisfies_any_imp_NG.
(* Goal: F (IZR Z0) *)
apply Hany.
(* Goal: NG_existence_prop F (fun a b : R => Rle (Rabs a) (Rabs b)) *)
(* Goal: round_pred_total (Rnd_NA_pt F) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
intros x d u Hf Hd Hu.
(* Goal: or (Rle (Rabs x) (Rabs u)) (Rle (Rabs x) (Rabs d)) *)
(* Goal: round_pred_total (Rnd_NA_pt F) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
destruct (Rle_lt_dec 0 x) as [Hx|Hx].
(* Goal: or (Rle (Rabs x) (Rabs u)) (Rle (Rabs x) (Rabs d)) *)
(* Goal: or (Rle (Rabs x) (Rabs u)) (Rle (Rabs x) (Rabs d)) *)
(* Goal: round_pred_total (Rnd_NA_pt F) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
left.
(* Goal: Rle (Rabs x) (Rabs u) *)
(* Goal: or (Rle (Rabs x) (Rabs u)) (Rle (Rabs x) (Rabs d)) *)
(* Goal: round_pred_total (Rnd_NA_pt F) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
rewrite Rabs_pos_eq with (1 := Hx).
(* Goal: Rle x (Rabs u) *)
(* Goal: or (Rle (Rabs x) (Rabs u)) (Rle (Rabs x) (Rabs d)) *)
(* Goal: round_pred_total (Rnd_NA_pt F) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
rewrite Rabs_pos_eq.
(* Goal: Rle x u *)
(* Goal: or (Rle (Rabs x) (Rabs u)) (Rle (Rabs x) (Rabs d)) *)
(* Goal: round_pred_total (Rnd_NA_pt F) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
apply Hu.
(* Goal: Rle (IZR Z0) u *)
(* Goal: or (Rle (Rabs x) (Rabs u)) (Rle (Rabs x) (Rabs d)) *)
(* Goal: round_pred_total (Rnd_NA_pt F) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
apply Rle_trans with (1 := Hx).
(* Goal: Rle x u *)
(* Goal: or (Rle (Rabs x) (Rabs u)) (Rle (Rabs x) (Rabs d)) *)
(* Goal: round_pred_total (Rnd_NA_pt F) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
apply Hu.
(* Goal: or (Rle (Rabs x) (Rabs u)) (Rle (Rabs x) (Rabs d)) *)
(* Goal: round_pred_total (Rnd_NA_pt F) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
right.
(* Goal: Rle (Rabs x) (Rabs d) *)
(* Goal: round_pred_total (Rnd_NA_pt F) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
rewrite Rabs_left with (1 := Hx).
(* Goal: Rle (Ropp x) (Rabs d) *)
(* Goal: round_pred_total (Rnd_NA_pt F) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
rewrite Rabs_left1.
(* Goal: Rle (Ropp x) (Ropp d) *)
(* Goal: Rle d (IZR Z0) *)
(* Goal: round_pred_total (Rnd_NA_pt F) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
apply Ropp_le_contravar.
(* Goal: Rle d x *)
(* Goal: round_pred_total (Rnd_NA_pt F) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
apply Hd.
(* Goal: Rle d (IZR Z0) *)
(* Goal: round_pred_total (Rnd_NA_pt F) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
apply Rlt_le in Hx.
(* Goal: Rle d (IZR Z0) *)
(* Goal: round_pred_total (Rnd_NA_pt F) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
apply Rle_trans with (2 := Hx).
(* Goal: Rle d x *)
(* Goal: round_pred_total (Rnd_NA_pt F) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
apply Hd.
(* Goal: round_pred_total (Rnd_NA_pt F) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
intros x.
(* Goal: @ex R (fun f : R => Rnd_NA_pt F x f) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
destruct (H x) as (f, Hf).
(* Goal: @ex R (fun f : R => Rnd_NA_pt F x f) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
exists f.
(* Goal: Rnd_NA_pt F x f *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
apply <- Rnd_NA_NG_pt.
(* Goal: Rnd_NG_pt F (fun x f : R => Rle (Rabs x) (Rabs f)) x f *)
(* Goal: F (IZR Z0) *)
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
apply Hf.
(* Goal: F (IZR Z0) *)
apply Hany.
(* Goal: round_pred_monotone (Rnd_NA_pt F) *)
apply Rnd_NA_pt_monotone.
(* Goal: F (IZR Z0) *)
apply Hany.
Qed.

End RND_prop.
