proposition: Theorem Babs_Bopp : forall abs_nan opp_nan x, is_nan x = false -> Babs abs_nan (Bopp opp_nan x) = Babs abs_nan x.
proof: Proof. now intros abs_nan opp_nan [| | |]. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative BinarySingleNaN