proposition: Theorem Bopp_involutive : forall opp_nan x, is_nan x = false -> Bopp opp_nan (Bopp opp_nan x) = x.
proof: Proof. now intros opp_nan [sx|sx|sx plx|sx mx ex Hx] ; simpl ; try rewrite Bool.negb_involutive. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative BinarySingleNaN