proposition: Lemma float_absolute_n_whole : forall c p d k x, (Rabs x < bpow radix2 k)%R -> (Rabs (rounding_float (Znearest c) p d x - x) <= bpow radix2 (FLT_exp d (Zpos p) k - 1))%R.
proof: Proof. Proof with auto with typeclass_instances. intros c p d k x Hx. destruct (Req_dec x 0) as [Hx0|Hx0]. rewrite Hx0, round_0, Rminus_0_r, Rabs_R0... apply bpow_ge_0. apply Rle_trans with (/2 * ulp radix2 (FLT_exp d (Zpos p)) x)%R. apply error_le_half_ulp... rewrite ulp_neq_0; trivial. rewrite <- (bpow_plus radix2 (-1)). apply bpow_le. unfold Zminus. rewrite (Zplus_comm _ (-1)). apply Zplus_le_compat_l. unfold cexp. apply monotone_exp... now apply mag_le_bpow. 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