proposition: Lemma aux_2 : generic_format radix2 (fexp prec emax) (Rpow2 53 - 1).
proof: Proof. simpl. rewrite <-minus_IZR. simpl. apply generic_format_FLT. exists (Float radix2 9007199254740991 0); [| easy..]. unfold F2R. simpl. symmetry. apply Rmult_1_r. Qed.
imports: Coq(PrimInt63 Sint63 Floats PArray) Coq(Bool List Reals Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations)