proposition: Theorem is_finite_Bopp : forall opp_nan x, is_finite (Bopp opp_nan x) = is_finite x.
proof: Proof. now intros opp_nan [| | |]. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative BinarySingleNaN