proposition: Theorem round_opp : forall x, round rnd (- x) = Ropp (round Zrnd_opp x).
proof: Proof. intros x. unfold round. rewrite <- F2R_Zopp, cexp_opp, scaled_mantissa_opp. apply F2R_eq. apply sym_eq. exact (Z.opp_involutive _). Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Float_prop