proposition: Lemma kLe2: (k <= Zceil (IZR(radix_val beta)/ 2) -1)%Z.
proof: Proof. cut (Zceil (x * bpow (1 - mag beta x) / (2+bpow (1-prec))) <= Zceil (IZR(radix_val beta)/ 2))%Z. unfold k; lia. apply Zceil_glb. apply Rle_trans with (bpow 1 / 2). unfold Rdiv; apply Rmult_le_compat. apply Rmult_le_pos. now left. apply bpow_ge_0. apply Rlt_le, Rinv_0_lt_compat. apply Rplus_lt_0_compat. now apply IZR_lt. apply bpow_gt_0. apply Rle_trans with (bpow (mag beta x)*bpow (1 - mag beta x)). apply Rmult_le_compat_r. apply bpow_ge_0. apply Rle_trans with (1:=RRle_abs _). left; apply bpow_mag_gt. rewrite <- bpow_plus. apply bpow_le; lia. apply Rinv_le. apply Rle_lt_0_plus_1, Rlt_le, Rlt_0_1. apply Rplus_le_reg_l with (-2); ring_simplify. apply bpow_ge_0. rewrite bpow_1. apply Zceil_ub. Qed.
imports: Coq(Reals Psatz) Flocq(Core) Interval(Tactic)