proposition: Lemma format_is_pff_format: forall r, (generic_format beta (FLT_exp (-dExp b) p) r) -> exists f, FtoR beta f = r /\ Fbounded b f.
proof: Proof. intros r Hr. eexists; split. 2: apply (format_is_pff_format' _ Hr). rewrite Hr at 3; unfold FtoR, F2R; simpl. now rewrite bpow_powerRZ. Qed.
imports: Coq(Lia) Pff Core