proposition: Lemma kLe: (k < radix_val beta)%Z.
proof: Proof. cut (Zceil (x * bpow (1 - mag beta x) / (2+bpow (1-prec))) <= beta)%Z. unfold k; lia. apply Zceil_glb. apply Rle_trans with (bpow 1 / 1). unfold Rdiv; apply Rmult_le_compat. apply Rmult_le_pos; try apply bpow_ge_0; now left. 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. exact Rlt_0_1. apply Rplus_le_reg_l with (-1); ring_simplify. apply Rlt_le, Rle_lt_0_plus_1, bpow_ge_0. rewrite bpow_1; right; field. Qed.
imports: Coq(Reals Psatz) Flocq(Core) Interval(Tactic)