proposition: Lemma round_NE_is_pff_round_b64: forall (r:R), exists f:Pff.float, (Fcanonic 2 bdouble f /\ (EvenClosest bdouble 2 53 r f) /\ FtoR 2 f = round radix2 (FLT_exp (-1074) 53) rndNE r).
proof: Proof. apply (round_NE_is_pff_round radix2 bdouble 53). apply pdGivesBound. apply eq_refl. Qed.
imports: Coq(Lia) Pff Core