proposition: Lemma compare_antisym_eq : forall x y c, (x?=y = CompOpp c) <-> (y?=x = c).
proof: Proof. intros. rewrite <- (compare_antisym y x). split; intro. rewrite CompOpp_eq in H. hyp. rewrite H. refl. Qed.
imports: CoLoR(LogicUtil BigNUtil NatUtil) Coq(ZArith) CoLoR(OrdUtil)