proposition: Lemma round_N_is_pff_round: forall choice, forall (r:R), exists f:Pff.float, (Fcanonic beta b f /\ (Closest b beta r f) /\ FtoR beta f = round beta (FLT_exp (-dExp b) p) (Znearest choice) r).
proof: Proof. intros choice r. assert (1 < Z.abs_nat p). apply Nat2Z.inj_lt; simpl. rewrite inj_abs; lia. exists (RND_Closest b beta (Z.abs_nat p) choice r); split. apply RND_Closest_canonic; easy. split. apply RND_Closest_correct; easy. apply pff_round_N_is_round. Qed.
imports: Coq(Lia) Pff Core