proposition: Lemma fexp_emax : fexp emax = (emax - prec)%Z.
proof: Proof. apply Z.max_l. unfold emin. unfold Prec_gt_0 in prec_gt_0_. unfold Prec_lt_emax in prec_lt_emax_. lia. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative