proposition: Theorem cexp_fexp : forall x ex, (bpow (ex - 1) <= Rabs x < bpow ex)%R -> cexp x = fexp ex.
proof: Proof. intros x ex Hx. unfold cexp. now rewrite mag_unique with (1 := Hx). Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Float_prop