proposition: Theorem flt_of_fix_bnd : forall x xi n p, FIX x n -> ABS x xi -> Zle_bool (Zpos (digits (pos_of_Z (Fnum (upper xi)))) + Fexp (upper xi)) (n + Zpos p) = true -> FLT x p.
proof: Proof. intros x (xl,(mu,eu)) n p ((m,e),(Hx1,Hx2)) Hxi H. generalize (Zle_bool_imp_le _ _ H). clear H. intro H. exists (Float2 m e). split. exact Hx1. unfold float2R in Hx1. simpl in Hx1. simpl Fnum in H. simpl Fexp in H. apply (lt_F2R radix2 e). rewrite F2R_Zabs. apply Rle_lt_trans with (F2R (Float radix2 mu eu)). simpl. rewrite Hx1. apply Hxi. apply Rlt_le_trans with (bpow radix2 (n + Zpos p)). destruct (Zle_or_lt mu 0) as [Hu|Hu]. apply Rle_lt_trans with R0. now apply F2R_le_0. apply bpow_gt_0. apply Rlt_le_trans with (bpow radix2 (Digits.Zdigits radix2 mu + eu)). rewrite Zdigits_mag. 2: intros Hu' ; now rewrite Hu' in Hu. rewrite <- mag_F2R. 2: intros Hu' ; now rewrite Hu' in Hu. destruct (mag radix2 (F2R (Float radix2 mu eu))) as (e', He). apply (Rle_lt_trans _ _ _ (RRle_abs _)). apply He. apply Rgt_not_eq. now apply F2R_gt_0. rewrite <- (Zpos_pos_of_Z _ Hu). rewrite <- digits2_digits. now apply bpow_le. unfold F2R. simpl. change (Zpower_pos 2 p) with (Zpower radix2 (Zpos p)). rewrite IZR_Zpower. 2: easy. rewrite <- bpow_plus. apply bpow_le. rewrite Zplus_comm. now apply Zplus_le_compat_l. Qed.
imports: Flocq(Core Sterbenz) Gappa_common Gappa_round_aux