proposition: Lemma fourth_format_2: forall prec:Z, (0 < prec)%Z -> generic_format radix2 (FLX_exp prec) (/4).
proof: Proof. Proof with auto with typeclass_instances. intros prec Hprec. change (/4)%R with (bpow radix2 (-2)). apply generic_format_bpow'... unfold FLX_exp. lia. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core Relative Sterbenz Operations) Interval(Tactic)