proposition: Theorem Bcompare_swap : forall x y, Bcompare y x = match Bcompare x y with Some c => Some (CompOpp c) | None => None end.
proof: Proof. intros. apply BinarySingleNaN.Bcompare_swap. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative BinarySingleNaN