proposition: Theorem mag_DN : forall x, (0 < round Zfloor x)%R -> (mag beta (round Zfloor x) = mag beta x :> Z).
proof: Proof. intros x Hd. assert (0 < x)%R. apply Rlt_le_trans with (1 := Hd). apply round_DN_pt. revert Hd. rewrite <- round_ZR_DN. intros Hd. apply mag_round_ZR. now apply Rgt_not_eq. now apply Rlt_le. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Float_prop