proposition: Lemma pff_format_is_format: forall f, Fbounded b f -> (generic_format beta (FLT_exp (-dExp b) p) (FtoR beta f)).
proof: Proof. intros f Hf. apply generic_format_FLT; auto with zarith. exists (Float beta (Pff.Fnum f) (Pff.Fexp f)). unfold F2R, FtoR; simpl. rewrite bpow_powerRZ. reflexivity. destruct Hf. apply Z.lt_le_trans with (1:=H). rewrite pGivesBound. rewrite Zpower_Zpower_nat; auto with zarith. now destruct Hf. Qed.
imports: Coq(Lia) Pff Core