proposition: Theorem round_ZR_DN : forall x, (0 <= x)%R -> round Ztrunc x = round Zfloor x.
proof: Proof. intros x Hx. unfold round, Ztrunc. case Rlt_bool_spec. intros 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. easy. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Float_prop