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