proposition: Theorem flt_float_of_flt : forall rdir {Hrnd : Valid_rnd rdir} p d xn zn x, FLT x xn -> Zle_bool (Zpos xn) (Zpos zn) = true -> FLT (rounding_float rdir p d x) zn.
proof: Proof. Proof with auto with typeclass_instances. intros rdir Hrnd p d xn zn x H Hb. generalize (Zle_bool_imp_le _ _ Hb). clear Hb. intro H1. apply FLT_iff_generic. apply generic_round_generic... apply FLT_iff_generic. now apply flt_le with xn. Qed.
imports: Coq(Bool ZArith Reals Lia) Flocq(Core Digits Round Relative) Gappa_definitions Gappa_dyadic Gappa_pred_bnd Gappa_round_def Gappa_round_aux Gappa_round