proposition: Theorem abs_lt_bpow_prec: forall prec, (forall e, (e - prec <= fexp e)%Z) -> forall x, (Rabs x < bpow (prec + cexp x))%R.
proof: Proof. intros prec Hp x. case (Req_dec x 0); intros Hxz. rewrite Hxz, Rabs_R0. apply bpow_gt_0. unfold cexp. destruct (mag beta x) as (ex,Ex) ; simpl. specialize (Ex Hxz). apply Rlt_le_trans with (1 := proj2 Ex). apply bpow_le. specialize (Hp ex). lia. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Float_prop