proposition: Theorem fixed_error_n : forall c e x zi, fixed_error_n_helper e zi = true -> BND (rounding_fixed (Znearest c) e x - x) zi.
proof: Proof. intros c e x zi Hb. generalize (andb_prop _ _ Hb). clear Hb. intros (H1,H2). generalize (Fle2_correct _ _ H1). clear H1. intro H1. generalize (Fle2_correct _ _ H2). clear H2. intro H2. assert (H := error_le_half_ulp radix2 (FIX_exp e) c x). replace (/2 * ulp radix2 (FIX_exp e) x)%R with (float2R (Float2 1 (e - 1))) in H. destruct (Rabs_le_inv _ _ H) as (H3,H4). split. apply Rle_trans with (1 := H1). unfold float2R. now rewrite (F2R_Zopp _ 1%Z). now apply Rle_trans with (2 := H2). rewrite ulp_FIX. unfold float2R, Zminus. rewrite F2R_bpow, Zplus_comm. apply bpow_plus. Qed.
imports: Bool ZArith Reals Flocq.Core.Core Gappa_definitions Gappa_dyadic Gappa_pred_bnd Gappa_round_def Gappa_round_aux Gappa_round