proposition: Theorem floatx_of_flt : forall rdir {Hrnd : Valid_rnd rdir}, forall x : R, forall p1 p2 : positive, FLT x p1 -> Zle_bool (Zpos p1) (Zpos p2) = true -> rounding_floatx rdir p2 x = x.
proof: Proof. Proof with auto with typeclass_instances. intros rdir Hrnd x p1 p2 [[m e] [Hx1 Hx2]] Hb. generalize (Zle_bool_imp_le _ _ Hb). clear Hb. intro H1. apply round_generic... rewrite <- Hx1. apply generic_format_F2R. unfold cexp. intros Hm ; simpl. rewrite mag_F2R with (1 := Hm). simpl. unfold FLX_exp. cut (mag radix2 (IZR m) <= Zpos p1)%Z. clear -H1 ; lia. apply bpow_lt_bpow with radix2. destruct (mag radix2 (IZR m)) as [n Hn]. simpl. specialize (Hn (IZR_neq _ _ Hm)). apply Rle_lt_trans with (1 := proj1 Hn). rewrite <- abs_IZR. now apply IZR_lt. 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