proposition: Lemma format_is_pff_format': forall r, (generic_format beta (FLT_exp (-dExp b) p) r) -> Fbounded b (Pff.Float (Ztrunc (scaled_mantissa beta (FLT_exp (-dExp b) p) r)) (cexp beta (FLT_exp (-dExp b) p) r)).
proof: Proof. intros x; unfold generic_format. set (ex := cexp beta (FLT_exp (-dExp b) p) x). set (mx := Ztrunc (scaled_mantissa beta (FLT_exp (-dExp b) p) x)). intros Hx; repeat split ; simpl. apply lt_IZR. rewrite pGivesBound, IZR_Zpower_nat. apply Rmult_lt_reg_r with (bpow beta ex). apply bpow_gt_0. rewrite <- bpow_plus. rewrite inj_abs; try lia. change (F2R (Float beta (Z.abs mx) ex) < bpow beta (p + ex))%R. rewrite F2R_Zabs. rewrite <- Hx. destruct (Req_dec x 0) as [Hx0|Hx0]. rewrite Hx0, Rabs_R0. apply bpow_gt_0. unfold cexp in ex. destruct (mag beta x) as (ex', He). simpl in ex. specialize (He Hx0). apply Rlt_le_trans with (1 := proj2 He). apply bpow_le. cut (ex' - p <= ex)%Z. lia. unfold ex, FLT_exp. apply Z.le_max_l. apply Z.le_max_r. Qed.
imports: Coq(Lia) Pff Core