proposition: Theorem fix_of_fixed : forall rdir, forall x : R, forall k1 k2 : Z, Zle_bool k2 k1 = true -> FIX (rounding_fixed rdir k1 x) k2.
proof: Proof. intros rdir x k1 k2 H. generalize (Zle_bool_imp_le _ _ H). clear H. intro H. unfold FIX. eexists (Float2 _ _) ; repeat split. exact H. Qed.
imports: Bool ZArith Reals Flocq.Core.Core Gappa_definitions Gappa_dyadic Gappa_pred_bnd Gappa_round_def Gappa_round_aux Gappa_round