proposition: Theorem bnd_of_bnd_fix : forall x xn xi zi, BND x xi -> FIX x xn -> bnd_of_bnd_fix_helper xi zi xn = true -> BND x zi.
proof: Proof. Proof with auto with typeclass_instances. intros x xn xi zi Hxb ((m,e),(Hx1,Hx2)) Hb. generalize (andb_prop _ _ Hb). clear Hb. intros (H1,H2). generalize (Fle2_correct _ _ H1). rewrite (rndG_conversion roundUP_cs). clear H1. intro H1. generalize (Fle2_correct _ _ H2). rewrite (rndG_conversion roundDN_cs). clear H2. intro H2. rewrite <- Hx1. rewrite <- Hx1 in Hxb. split. apply Rle_trans with (1 := H1). unfold float2R at 2. simpl. rewrite <- (round_generic radix2 (FIX_exp xn) Zceil (F2R (Float radix2 m e))). apply round_le... apply Hxb. now apply generic_format_F2R. apply Rle_trans with (2 := H2). unfold float2R at 1. simpl. rewrite <- (round_generic radix2 (FIX_exp xn) Zfloor (F2R (Float radix2 m e))). apply round_le... apply Hxb. now apply generic_format_F2R. Qed.
imports: Bool ZArith Reals Flocq.Core.Core Gappa_definitions Gappa_dyadic Gappa_pred_bnd Gappa_round_def Gappa_round_aux Gappa_round