proposition: Theorem fixed_error_up : forall e x zi, fixed_error_up_helper e zi = true -> BND (rounding_fixed rndUP 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 (Fneg0_correct _ H1). clear H1. intro H1. generalize (Fle2_correct _ _ H2). clear H2. intro H2. split. - apply Rle_trans with (1 := H1). apply Rle_0_minus. apply round_UP_pt... - apply Rle_trans with (2 := H2). destruct (Rabs_le_inv _ _ (error_le_ulp radix2 (FIX_exp e) Zceil x)) as [_ H]. rewrite ulp_FIX in H. unfold float2R. now rewrite F2R_bpow. Qed.
imports: Bool ZArith Reals Flocq.Core.Core Gappa_definitions Gappa_dyadic Gappa_pred_bnd Gappa_round_def Gappa_round_aux Gappa_round