proposition: Theorem cexp_DN : forall x, (0 < round Zfloor x)%R -> cexp (round Zfloor x) = cexp x.
proof: Proof. intros x Hd. apply (f_equal fexp). now apply mag_DN. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Float_prop