proposition: Theorem cexp_fexp_pos : forall x ex, (bpow (ex - 1) <= x < bpow ex)%R -> cexp x = fexp ex.
proof: Proof. intros x ex Hx. apply cexp_fexp. rewrite Rabs_pos_eq. exact Hx. apply Rle_trans with (2 := proj1 Hx). apply bpow_ge_0. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Float_prop