proposition: Theorem round_NE_pt : forall x, Rnd_NE_pt x (round beta fexp ZnearestE x).
proof: Proof. Proof with auto with typeclass_instances. intros x. destruct (total_order_T x 0) as [[Hx|Hx]|Hx]. apply Rnd_NG_pt_opp_inv. apply generic_format_opp. unfold NE_prop. intros _ f ((mg,eg),(H1,(H2,H3))). exists (Float beta (- mg) eg). repeat split. rewrite H1. now rewrite F2R_Zopp. now apply canonical_opp. simpl. now rewrite Z.even_opp. rewrite <- round_NE_opp. apply round_NE_pt_pos. now apply Ropp_0_gt_lt_contravar. rewrite Hx, round_0... apply Rnd_NG_pt_refl. apply generic_format_0. now apply round_NE_pt_pos. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Generic_fmt Float_prop Ulp