proposition: Lemma FtoR_F2R: forall (f:Pff.float) (g: float beta), Pff.Fnum f = Fnum g -> Pff.Fexp f = Fexp g -> FtoR beta f = F2R g.
proof: Proof. intros f g H1 H2; unfold FtoR, F2R. rewrite H1, H2. now rewrite bpow_powerRZ. Qed.
imports: Coq(Lia) Pff Core