proposition: Lemma float_relative_inv_n_whole : forall c p d x, (bpow radix2 (d + Zpos p - 1) < Rabs (rounding_float (Znearest c) p d x))%R -> (Rabs ((rounding_float (Znearest c) p d x - x) / x) <= bpow radix2 (-Zpos p))%R.
proof: Proof. Proof with auto with typeclass_instances. intros c p d x Hx. apply float_relative_n_whole. apply Rnot_lt_le. contradict Hx. apply Rle_not_lt. apply abs_round_le_generic... apply generic_format_bpow. unfold FLT_exp. ring_simplify (d + Zpos p - 1 + 1 - Zpos p)%Z. rewrite Zmax_idempotent. clear ; zify ; lia. now apply Rlt_le. Qed.
imports: Coq(Bool ZArith Reals Lia) Flocq(Core Digits Round Relative) Gappa_definitions Gappa_dyadic Gappa_pred_bnd Gappa_round_def Gappa_round_aux Gappa_round