proposition: Theorem Bsign_Bone : Bsign Bone = false.
proof: Proof. generalize Bone_correct is_finite_strict_Bone. destruct Bone as [sx|sx| |[|] mx ex Bx] ; try easy. intros H _. contradict H. apply Rlt_not_eq, Rlt_trans with (2 := Rlt_0_1). now apply F2R_lt_0. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative