proposition: Theorem scaled_mantissa_DN : forall x, (0 < round Zfloor x)%R -> scaled_mantissa (round Zfloor x) = IZR (Zfloor (scaled_mantissa x)).
proof: Proof. intros x Hd. unfold scaled_mantissa. rewrite cexp_DN with (1 := Hd). unfold round, F2R. simpl. now rewrite Rmult_assoc, <- bpow_plus, Zplus_opp_r, Rmult_1_r. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Float_prop