proposition: Lemma kpos: (0 <= k)%Z.
proof: Proof. assert (0 < x*bpow (1-mag beta x)/(2+bpow (1-prec))). apply Fourier_util.Rlt_mult_inv_pos. apply Rmult_lt_0_compat. assumption. apply bpow_gt_0. apply Rplus_lt_0_compat. now apply IZR_lt. apply bpow_gt_0. assert (0 < Zceil (x * bpow (1 - mag beta x) / (2+bpow (1-prec))))%Z. apply lt_IZR. apply Rlt_le_trans with (1:=H). apply Zceil_ub. unfold k; lia. Qed.
imports: Coq(Reals Psatz) Flocq(Core) Interval(Tactic)