proposition: Theorem round_DN_opp : forall x, round Zfloor (-x) = (- round Zceil x)%R.
proof: Proof. intros x. unfold round. rewrite scaled_mantissa_opp. rewrite <- F2R_Zopp. unfold Zceil. rewrite Z.opp_involutive. now rewrite cexp_opp. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Float_prop