proposition: Theorem fixed_of_fix : forall rdir {Hrnd : Valid_rnd rdir} x e1 e2, FIX x e1 -> Zle_bool e2 e1 = true -> rounding_fixed rdir e2 x = x.
proof: Proof. intros rdir Hrnd x e1 e2 ((m,e),(Hx1,Hx2)) H1. generalize (Zle_bool_imp_le _ _ H1). clear H1. intro H1. apply round_generic with (1 := Hrnd). rewrite <- Hx1. apply generic_format_F2R. intros _. now apply Z.le_trans with e1. Qed.
imports: Bool ZArith Reals Flocq.Core.Core Gappa_definitions Gappa_dyadic Gappa_pred_bnd Gappa_round_def Gappa_round_aux Gappa_round