proposition: Theorem fix_of_flt_bnd : forall x : R, forall xi : FF, forall n : Z, forall p : positive, FLT x p -> ABS x xi -> Zle_bool (n + Zpos p) (Zpos (digits (pos_of_Z (Fnum (lower xi)))) + Fexp (lower xi)) && Fpos (lower xi) = true -> FIX x n.
proof: Proof. intros x ((ml,el),xu) n p ((mx,ex),(Hx1,Hx2)) (_,(Hxi,_)) Hb. generalize (andb_prop _ _ Hb). clear Hb. intros (H1,H2). generalize (Zle_bool_imp_le _ _ H1). simpl Fnum. simpl Fexp. clear H1. intro H1. generalize (Fpos_correct _ H2). simpl. clear H2. intro H2. exists (Float2 mx ex). split. exact Hx1. apply Zplus_le_reg_l with (Zpos p). rewrite Zplus_comm. apply Z.le_trans with (1 := H1). clear H1. rewrite digits2_digits. assert (H0: (0 < ml)%Z). apply gt_0_F2R with (1 := H2). rewrite Zpos_pos_of_Z with (1 := H0). assert (H0': ml <> Z0). intros H. now rewrite H in H0. rewrite Zdigits_mag with (1 := H0'). rewrite <- mag_F2R with (1 := H0'). apply Z.le_trans with (mag radix2 (Rabs (Float2 mx ex))). apply mag_le. now apply F2R_gt_0. now rewrite Hx1. rewrite mag_abs. unfold float2R. assert (Hx0: mx <> Z0). intros H. apply Rle_not_lt with (1 := Hxi). rewrite <- Hx1, H. unfold float2R. rewrite F2R_0, Rabs_R0. now apply F2R_gt_0. rewrite mag_F2R with (1 := Hx0). apply Zplus_le_compat_r. destruct (mag radix2 (IZR mx)) as (e, He). simpl. apply bpow_lt_bpow with radix2. apply Rle_lt_trans with (Rabs (IZR mx)). apply He. now apply (IZR_neq _ 0%Z). rewrite <- abs_IZR. rewrite <- IZR_Zpower. 2: easy. now apply IZR_lt. Qed.
imports: Flocq(Core Sterbenz) Gappa_common Gappa_round_aux