proposition: Lemma xkgt: bpow (mag beta x - 1) < xk.
proof: Proof. unfold xk. case kradix2. intros V; rewrite V; simpl; ring_simplify. apply Rle_lt_trans with (2:=Hx). rewrite <- (Rmult_1_l (bpow (mag beta x - 1))) at 1. apply Rmult_le_compat_r. apply bpow_ge_0. assert (2 <= beta)%Z. clear; destruct beta as (v, Hr); simpl. now apply Zle_bool_imp_le. apply IZR_le in H. simpl in H; interval with (i_prec 30). intros Hb. apply Rle_lt_trans with (sqrt (IZR beta) * bpow (mag beta x - 1) - IZR k * ulp_flx x). rewrite ulp_neq_0; try now apply Rgt_not_eq. unfold cexp, FLX_exp. apply Rle_trans with (bpow (mag beta x - 1) *(sqrt (IZR beta) -IZR k * bpow (1-prec))). rewrite <- (Rmult_1_r (bpow (mag beta x - 1))) at 1. apply Rmult_le_compat_l. apply bpow_ge_0. apply Rplus_le_reg_l with (IZR k * bpow (1 - prec)). apply Rle_trans with ((1-/IZR beta) * bpow (2 - prec)+1). apply Rplus_le_compat_r. apply Rle_trans with (((1-/IZR beta)*IZR beta) * bpow (1 - prec)). apply Rmult_le_compat_r. apply bpow_ge_0. apply Rle_trans with (IZR (beta-1)). apply IZR_le. lia. rewrite minus_IZR; right. simpl; field. apply Rgt_not_eq, Rlt_gt. apply IZR_lt, radix_gt_0. right; rewrite Rmult_assoc; apply f_equal. rewrite <- bpow_1, <- bpow_plus. apply f_equal; ring. ring_simplify (IZR k * bpow (1 - prec) + (sqrt (IZR beta) - IZR k * bpow (1 - prec))). assert (H':(3 <= beta)%Z) by lia. apply IZR_le in H'; simpl in H'. assert (H'':(1 <= IZR beta)). apply Rle_trans with (2:=H'). apply Rplus_le_reg_l with (-1); ring_simplify. auto with real. case (Zle_lt_or_eq 3 beta). lia. intros H1; assert (H1':(4 <= beta)%Z) by lia. apply IZR_le in H1'; simpl in H1'. apply Rle_trans with (1*1 +1). apply Rplus_le_compat_r. apply Rmult_le_compat. apply Rplus_le_reg_l with (/IZR beta); ring_simplify. rewrite <- Rinv_1. apply Rle_Rinv. apply Rlt_0_1. apply Rlt_le_trans with (2:=H''); auto with real. exact H''. apply bpow_ge_0. apply Rplus_le_reg_l with (/IZR beta-1); ring_simplify. left; apply Rinv_0_lt_compat. apply Rlt_le_trans with (2:=H''); auto with real. apply Rle_trans with (bpow 0). apply bpow_le. lia. right; reflexivity. interval with (i_prec 30). intros Hb'. apply Rle_trans with ((1 - / IZR beta) *1 +1). apply Rplus_le_compat_r. apply Rmult_le_compat_l. apply Rplus_le_reg_l with (/IZR beta); ring_simplify. rewrite <- Rinv_1. apply Rle_Rinv. apply Rlt_0_1. apply Rlt_le_trans with (2:=H''); auto with real. exact H''. apply Rle_trans with (bpow 0). apply bpow_le. lia. right; reflexivity. rewrite <- Hb'; simpl; interval. right; ring_simplify. apply f_equal. apply trans_eq with (IZR k *(bpow (mag beta x - 1) * bpow (1 - prec))). ring. apply f_equal. rewrite <- bpow_plus. apply f_equal. ring. apply Rplus_lt_compat_r. assumption. Qed.
imports: Coq(Reals Psatz) Flocq(Core) Interval(Tactic)