proposition: Theorem fix_of_float : forall rdir x p k1 k2, Zle_bool k2 k1 = true -> FIX (rounding_float rdir p k1 x) k2.
proof: Proof. intros rdir x p k1 k2 H. generalize (Zle_bool_imp_le _ _ H). clear H. intro H. unfold FIX. eexists (Float2 _ _) ; repeat split. simpl. unfold cexp. apply Z.le_trans with (1 := H). apply Z.le_max_r. 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