proposition: Theorem cexp_inbetween_float : forall x m e l, (0 < x)%R -> inbetween_float beta m e x l -> (e <= cexp beta fexp x \/ e <= fexp (Zdigits beta m + e))%Z -> cexp beta fexp x = fexp (Zdigits beta m + e).
proof: Proof. intros x m e l Px Bx He. unfold cexp. apply inbetween_float_bounds in Bx. assert (0 <= m)%Z as Hm. { apply Zlt_succ_le. eapply gt_0_F2R. apply Rlt_trans with (1 := Px). apply Bx. } destruct (Zle_lt_or_eq _ _ Hm) as [Hm'|<-]. now erewrite <- mag_F2R_bounds_Zdigits with (1 := Hm'). clear Hm. assert (mag beta x <= e)%Z as Hx. { apply mag_le_bpow. now apply Rgt_not_eq. rewrite Rabs_pos_eq. now rewrite <- F2R_bpow. now apply Rlt_le. } simpl in He |- *. clear Bx. destruct He as [He|He]. - apply eq_sym, valid_exp with (2 := He). now apply Z.le_trans with e. - apply valid_exp with (1 := He). now apply Z.le_trans with e. Qed.
imports: Coq(ZArith Reals Lia) Core Digits Float_prop Bracket