proposition: Theorem Rnd_NE_pt_monotone : round_pred_monotone Rnd_NE_pt.
proof: Proof. apply Rnd_NG_pt_monotone. intros x d u Hd Hdn Hu Hun (cd, (Hd1, Hd2)) (cu, (Hu1, Hu2)). destruct (Req_dec x d) as [Hx|Hx]. rewrite <- Hx. apply sym_eq. apply Rnd_UP_pt_idempotent with (1 := Hu). rewrite Hx. apply Hd. rewrite (DN_UP_parity_aux DN_UP_parity_generic_pos x cd cu) in Hu2 ; try easy. now rewrite (proj2 Hd2) in Hu2. intros Hf. apply Hx. apply sym_eq. now apply Rnd_DN_pt_idempotent with (1 := Hd). rewrite <- Hd1. apply Rnd_DN_pt_unique with (1 := Hd). now apply round_DN_pt. rewrite <- Hu1. apply Rnd_UP_pt_unique with (1 := Hu). now apply round_UP_pt. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Generic_fmt Float_prop Ulp