proposition: Theorem fixed_round : forall rdir e x xi zi, BND x xi -> round_helper (round (rndG_g rdir) (FIX_exp e)) xi zi = true -> BND (rounding_fixed (rndG_f rdir) e x) zi.
proof: Proof. Proof with auto with typeclass_instances. intros rdir e x xi zi Hx Hb. generalize (andb_prop _ _ Hb). clear Hb. intros (H1,H2). generalize (Fle2_correct _ _ H1). rewrite rndG_conversion. clear H1. intro H1. generalize (Fle2_correct _ _ H2). rewrite rndG_conversion. clear H2. intro H2. split. apply Rle_trans with (1 := H1). apply round_le... apply Hx. apply Rle_trans with (2 := H2). apply round_le... apply Hx. Qed.
imports: Bool ZArith Reals Flocq.Core.Core Gappa_definitions Gappa_dyadic Gappa_pred_bnd Gappa_round_def Gappa_round_aux Gappa_round