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. unfold Bcompare. destruct x as [ ? | [] | | [] mx ex Bx ]; destruct y as [ ? | [] | | [] my ey By ]; simpl; try easy. - rewrite <- (Zcompare_antisym ex ey). destruct (ex ?= ey)%Z; try easy. now rewrite (Pcompare_antisym mx my). - rewrite <- (Zcompare_antisym ex ey). destruct (ex ?= ey)%Z; try easy. now rewrite Pcompare_antisym. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative