proposition: Theorem flt_of_floatx : forall rdir {Hrnd : Valid_rnd rdir} x p1 p2, Zle_bool (Zpos p1) (Zpos p2) = true -> FLT (rounding_floatx rdir p1 x) p2.
proof: Proof. Proof with auto with typeclass_instances. intros rdir Hrnd x p1 p2 H. generalize (Zle_bool_imp_le _ _ H). clear H. intro H. unfold FLT. destruct (FLX_format_generic radix2 (Zpos p1) (Generic_fmt.round radix2 (FLX_exp (Zpos p1)) rdir x)) as ((m, e), H1, H2). apply generic_format_round... rewrite H1. eexists (Float2 _ _) ; repeat split. apply Z.lt_le_trans with (1 := H2). change (Zpower_pos 2 p2) with (Zpower radix2 (Zpos p2)). now apply Zpower_le. 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