proposition: Theorem B2R_Babs : forall abs_nan x, B2R (Babs abs_nan x) = Rabs (B2R x).
proof: Proof. intros abs_nan [sx|sx|sx plx Hx|sx mx ex Hx]; apply sym_eq ; try apply Rabs_R0. simpl. rewrite <- F2R_abs. now destruct sx. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative BinarySingleNaN