proposition: Theorem cexp_inbetween_float_loc_Exact : forall x m e l, (0 <= x)%R -> inbetween_float beta m e x l -> (e <= cexp beta fexp x \/ l = loc_Exact <-> e <= fexp (Zdigits beta m + e) \/ l = loc_Exact)%Z.
proof: Proof. intros x m e l Px Bx. destruct Px as [Px|Px]. - split ; (intros [H|H] ; [left|now right]). rewrite <- cexp_inbetween_float with (1 := Px) (2 := Bx). exact H. now left. rewrite cexp_inbetween_float with (1 := Px) (2 := Bx). exact H. now right. - assert (H := Bx). destruct Bx as [|c Bx _]. now split ; right. rewrite <- Px in Bx. destruct Bx as [Bx1 Bx2]. apply lt_0_F2R in Bx1. apply gt_0_F2R in Bx2. lia. Qed.
imports: Coq(ZArith Reals Lia) Core Digits Float_prop Bracket