proposition: Theorem round_ZR_opp : forall x, round Ztrunc (- x) = Ropp (round Ztrunc x).
proof: Proof. intros x. unfold round. rewrite scaled_mantissa_opp, cexp_opp, Ztrunc_opp. apply F2R_Zopp. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Float_prop