proposition: Theorem fixed_error_dn : forall e x zi, fixed_error_dn_helper e zi = true -> BND (rounding_fixed rndDN e x - x) zi.
proof: Proof. Proof with auto with typeclass_instances. intros e x zi Hb. generalize (andb_prop _ _ Hb). clear Hb. intros (H1,H2). generalize (Fle2_correct _ _ H1). clear H1. intro H1. generalize (Fpos0_correct _ H2). clear H2. intro H2. split. apply Rle_trans with (1 := H1). destruct (Rabs_le_inv _ _ (error_le_ulp radix2 (FIX_exp e) Zfloor x)) as (H, _). rewrite ulp_FIX in H. unfold float2R. rewrite (F2R_Zopp _ 1%Z). now rewrite F2R_bpow. apply Rle_trans with (2 := H2). apply Rle_minus. apply round_DN_pt... Qed.
imports: Bool ZArith Reals Flocq.Core.Core Gappa_definitions Gappa_dyadic Gappa_pred_bnd Gappa_round_def Gappa_round_aux Gappa_round