proposition: Lemma round_N0_opp : forall x, (round Znearest0 (- x) = - round Znearest0 x)%R.
proof: Proof. intros 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 (- (Zfloor x + 1) <? 0)%Z = (Zfloor x <? 0)%Z); [|now rewrite H]. rewrite negb_Zlt_bool. case_eq (Zfloor x <? 0)%Z; intro C'. apply Zlt_is_lt_bool in C'. apply Zle_bool_true. lia. apply Z.ltb_ge in C'. apply Zle_bool_false. lia. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Float_prop