proposition: Lemma fourth_format_10: forall prec:Z, (2 <= prec)%Z -> generic_format radix10 (FLX_exp prec) (/4).
proof: Proof. Proof with auto with typeclass_instances. intros prec Hprec. apply generic_format_FLX. exists (Float radix10 25 (-2)). change (F2R (Float radix10 25 (-2))) with (25 / 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. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core Relative Sterbenz Operations) Interval(Tactic)