proposition: Lemma Bsign_Bopp : forall opp_nan x, is_nan x = false -> Bsign (Bopp opp_nan x) = negb (Bsign x).
proof: Proof. now intros opp_nan [s|s|s pl H|s m e H]. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative BinarySingleNaN