proposition: Lemma round_NE_is_pff_round_b32: forall (r:R), exists f:Pff.float, (Fcanonic 2 bsingle f /\ (EvenClosest bsingle 2 24 r f) /\ FtoR 2 f = round radix2 (FLT_exp (-149) 24) rndNE r).
proof: Proof. apply (round_NE_is_pff_round radix2 bsingle 24). apply psGivesBound. apply eq_refl. Qed.
imports: Coq(Lia) Pff Core