proposition: Lemma aux_3 : forall x', x' <= Rpow2 53 - 1 -> round radix2 (fexp prec emax) ZnearestE x' < Rpow2 53.
proof: Proof. intros x' Hx'. apply Rle_lt_trans with (Rpow2 53 - 1); [| lra]. now apply round_le_generic; [now apply FLT_exp_valid | apply valid_rnd_N | apply aux_2 |]. Qed.
imports: Coq(PrimInt63 Sint63 Floats PArray) Coq(Bool List Reals Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations)