proposition: Theorem fix_fixed_of_fix : forall rdir {Hrnd : Valid_rnd rdir} d xn zn x, FIX x xn -> Zle_bool zn xn = true -> FIX (rounding_fixed rdir d x) zn.
proof: Proof. Proof with auto with typeclass_instances. intros rdir Hrnd d xn zn x H Hb. generalize (Zle_bool_imp_le _ _ Hb). clear Hb. intro H1. apply FIX_iff_generic. apply generic_round_generic... apply FIX_iff_generic. now apply fix_le with xn. Qed.
imports: Bool ZArith Reals Flocq.Core.Core Gappa_definitions Gappa_dyadic Gappa_pred_bnd Gappa_round_def Gappa_round_aux Gappa_round