proposition: Theorem round_AW_DN : forall x, (x <= 0)%R -> round Zaway x = round Zfloor x.
proof: Proof. intros x Hx. unfold round, Zaway. case Rlt_bool_spec. easy. intros [H|H]. elim Rlt_not_le with (1 := H). rewrite <- (Rmult_0_l (bpow (- cexp x))). apply Rmult_le_compat_r with (2 := Hx). apply bpow_ge_0. rewrite <- H. now rewrite Zfloor_IZR, Zceil_IZR. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Float_prop