proposition: Lemma t4_exact_aux_: forall (f:float beta) g, (Z.abs (Fnum f) < Zpower beta prec)%Z -> (0 <= g <= F2R f)%R -> (exists n:Z, (g=IZR n*bpow (Fexp f))%R) -> (emin <= Fexp f)%Z -> format g.
proof: Proof. Proof with auto with typeclass_instances. intros f g Hf (Hg1,Hg2) (n,Hg3) Y. apply generic_format_FLT. exists (Float beta n (Fexp f)). exact Hg3. apply lt_IZR. rewrite IZR_Zpower. 2: lia. apply Rmult_lt_reg_r with (bpow (Fexp f)). apply bpow_gt_0. apply Rle_lt_trans with (F2R f). apply Rle_trans with (2:=Hg2). apply Rle_trans with (Rabs (F2R (Float beta n (Fexp f)))). rewrite <- F2R_Zabs. right; reflexivity. unfold F2R; simpl. rewrite <- Hg3. right; apply Rabs_right. now apply Rle_ge. rewrite <- (Rabs_right (F2R f)). replace (F2R f) with (F2R (Float beta (Fnum f) (Fexp f))) by reflexivity. rewrite <- F2R_Zabs. unfold F2R; apply Rmult_lt_compat_r. apply bpow_gt_0. rewrite <- IZR_Zpower. 2: lia. apply IZR_lt. now simpl. apply Rle_ge; apply Rle_trans with (1:=Hg1); assumption. assumption. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core Relative Sterbenz Operations) Interval(Tactic)