proposition: Lemma round_NE_is_pff_round: forall (r:R), exists f:Pff.float, (Fcanonic beta b f /\ (EvenClosest b beta (Z.abs_nat p) r f) /\ FtoR beta f = round beta (FLT_exp (-dExp b) p) rndNE r).
proof: Proof. intros r. exists (RND_EvenClosest b beta (Z.abs_nat p) r). split. apply RND_EvenClosest_canonic with (3 := pGivesBound). apply radix_gt_1. lia. split. apply RND_EvenClosest_correct with (3 := pGivesBound). apply radix_gt_1. lia. apply pff_round_NE_is_round. Qed.
imports: Coq(Lia) Pff Core