proposition: Theorem is_finite_strict_Bulp : forall x, is_finite_strict (Bulp x) = is_finite x.
proof: Proof. intros [sx|sx| |sx mx ex Bx] ; try easy. generalize (Bulp_correct (B754_finite sx mx ex Bx) eq_refl). destruct Bulp as [sy| | |] ; try easy. intros [H _]. contradict H. rewrite ulp_neq_0. apply Rlt_not_eq. apply bpow_gt_0. apply F2R_neq_0. now destruct sx. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative