proposition: Theorem round_NE_opp : forall x, round beta fexp ZnearestE (-x) = (- round beta fexp ZnearestE x)%R.
proof: Proof. intros x. unfold round. simpl. rewrite scaled_mantissa_opp, cexp_opp. rewrite Znearest_opp. rewrite <- F2R_Zopp. apply (f_equal (fun v => F2R (Float beta (-v) _))). set (m := scaled_mantissa beta fexp x). unfold Znearest. case Rcompare ; trivial. apply (f_equal (fun (b : bool) => if b then Zceil m else Zfloor m)). rewrite Bool.negb_involutive. rewrite Z.even_opp. rewrite Z.even_add. now rewrite eqb_sym. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Generic_fmt Float_prop Ulp