proposition: Lemma fourth_format_gen_2: forall prec emin e:Z, (0 < prec)%Z -> (emin +2 <= e)%Z -> generic_format radix2 (FLT_exp emin prec) (/4*bpow radix2 e).
proof: Proof. Proof with auto with typeclass_instances. intros prec emin e Hprec H. change (/4)%R with (bpow radix2 (-2)). rewrite <- bpow_plus. apply generic_format_bpow... unfold FLT_exp. lia. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core Relative Sterbenz Operations) Interval(Tactic)