proposition: Lemma round_N_opp_sym: forall x, round_flt (- x) = - round_flt x.
proof: Proof. intros x; unfold round; rewrite <- F2R_Zopp. rewrite cexp_opp; f_equal; f_equal. rewrite scaled_mantissa_opp. rewrite Znearest_opp. generalize (scaled_mantissa radix2 (FLT_exp emin prec) x). intros z; unfold Znearest; case (Rcompare _); try easy. now rewrite <- choice_sym. Qed.
imports: Psatz Core Plus_error Mult_error Operations Sterbenz Pff Pff2FlocqAux Nat2Z_compat