proposition: Lemma xklt: xk < bpow (mag beta x).
proof: Proof. apply Rle_lt_trans with x. apply Rplus_le_reg_l with (-xk); unfold xk; ring_simplify. apply Rmult_le_pos. apply IZR_le, kpos. apply ulp_ge_0. apply Rle_lt_trans with (1:=RRle_abs _). apply bpow_mag_gt. Qed.
imports: Coq(Reals Psatz) Flocq(Core) Interval(Tactic)