proposition: Lemma print17 : forall x, 0 < x -> generic_format radix2 (FLT_exp emin prec) x -> forall printed_x, Rabs (x - printed_x) <= /2 * bpow radix10 (mag radix10 x - 17) -> round radix2 (FLT_exp emin prec) (Znearest tie) printed_x = x.
proof: Proof. now apply print_generic; compute; [|lra]. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core)