proposition: Lemma fourth_format_gen_10: forall prec emin e:Z, (2 <= prec)%Z -> (emin +2 <= e)%Z -> generic_format radix10 (FLT_exp emin prec) (/4*bpow radix10 e).
proof: Proof. Proof with auto with typeclass_instances. intros prec emin e Hprec H. apply generic_format_FLT. exists (Float radix10 25 (e-2)). unfold F2R; simpl. unfold Zminus; rewrite bpow_plus. change (bpow radix10 (-(2))) with (/100)%R. field. simpl. apply Z.lt_le_trans with (10^2)%Z. unfold Zpower, Zpower_pos; simpl; lia. change 10%Z with (radix_val radix10). now apply Zpower_le. simpl. lia. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core Relative Sterbenz Operations) Interval(Tactic)