proposition: Lemma aux_4 : forall (x : binary_float prec emax), -2251799813685248 <= B2R x <= 2251799813685247 -> Rpow2 52 <= B2R x + B2R (Prim2B 6755399441055744) <= Rpow2 53 - 1.
proof: Proof. intros x Hx. cbn -[IZR Rplus Ropp Rmult Rinv]. unfold F2R; simpl. lra. Qed.
imports: Coq(PrimInt63 Sint63 Floats PArray) Coq(Bool List Reals Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations)