proposition: Lemma pcompare_prop: forall x y, Pos_as_OTA.compare x y = Eq <-> x = y.
proof: Proof. intros. intuition; psubst; trivial. Qed.
imports: ATBR(Common) ATBR(BoolView) ATBR(MyFSets MyFSetProperties MyFMapProperties) Coq(FSetPositive FMapPositive)