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