proposition: Lemma Bulp_correct_aux : bounded 1 emin = true.
proof: Proof. unfold bounded, canonical_mantissa. rewrite Zeq_bool_true. apply Zle_bool_true. apply Z.max_l_iff, fexp_emax. apply Z.max_r. simpl digits2_pos. generalize (prec_gt_0 prec). lia. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative