proposition: Theorem B2R_Bopp : forall x, B2R (Bopp x) = (- B2R x)%R.
proof: Proof. intros [sx|sx| |sx mx ex Hx]; apply sym_eq ; try apply Ropp_0. simpl. rewrite <- F2R_opp. now case sx. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative