proposition: Lemma format_is_pff_format_can: forall r, (generic_format beta (FLT_exp (-dExp b) p) r) -> exists f, FtoR beta f = r /\ Fcanonic beta b f.
proof: Proof. intros r Hr. destruct (format_is_pff_format r Hr) as (f,(Hf1,Hf2)). exists (Fnormalize beta b (Z.abs_nat p) f); split. rewrite <- Hf1; apply FnormalizeCorrect. apply radix_gt_1. apply FnormalizeCanonic; try assumption. apply radix_gt_1. lia. Qed.
imports: Coq(Lia) Pff Core