proposition: Lemma round_NA_opp : forall beta : radix, forall (fexp : Z -> Z), forall x, (round beta fexp ZnearestA (- x) = - round beta fexp ZnearestA x)%R.
proof: Proof. intros beta fexp x. rewrite round_N_opp. apply Ropp_eq_compat. apply round_ext. clear x; intro x. unfold Znearest. case_eq (Rcompare (x - IZR (Zfloor x)) (/ 2)); intro C; [|reflexivity|reflexivity]. apply Rcompare_Eq_inv in C. assert (H : negb (0 <=? - (Zfloor x + 1))%Z = (0 <=? Zfloor x)%Z); [|now rewrite H]. rewrite negb_Zle_bool. case_eq (0 <=? Zfloor x)%Z; intro C'. - apply Zle_bool_imp_le in C'. apply Zlt_bool_true. lia. - rewrite Z.leb_gt in C'. apply Zlt_bool_false. lia. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Float_prop