proposition: Lemma float_relative_n_whole : forall c p d x, (bpow radix2 (d + Zpos p - 1) <= Rabs x)%R -> (Rabs ((rounding_float (Znearest c) p d x - x) / x) <= bpow radix2 (-Zpos p))%R.
proof: Proof. intros c p d x Hx. assert (Hx0: x <> 0%R). intros Hx0. apply Rle_not_lt with (1 := Hx). rewrite Hx0, Rabs_R0. apply bpow_gt_0. destruct (relative_error_N_FLT_ex radix2 d (Zpos p) (refl_equal _) c x Hx) as (eps, (Hr1, Hr2)). rewrite Hr2. replace ((x * (1 + eps) - x) / x)%R with eps by now field. revert Hr1. rewrite <- (bpow_plus radix2 (-1)%Z). now rewrite (Zplus_comm (- Zpos p)), Zplus_assoc. 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