proposition: Lemma prec_suff_10: forall prec:Z, (3 <= prec)%Z -> (/2*bpow radix10 (1-prec) <= /100)%R.
proof: Proof. intros p Hp. apply Rle_trans with (/2* bpow radix10 (-2))%R. apply Rmult_le_compat_l. lra. apply bpow_le. lia. rewrite bpow_exp. change (IZR radix10) with 10%R. interval. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core Relative Sterbenz Operations) Interval(Tactic)