proposition: Lemma compare_spec : forall n m, BoolView.compare_spec eq lt n m (compare n m).
proof: Proof. intros. case_eq (compare n m); intro H; constructor. apply Pcompare_Eq_eq. apply H. apply H. unfold compare in H. apply ZC1. auto. Qed.
imports: ATBR(Common) ATBR(BoolView) ATBR(MyFSets MyFSetProperties MyFMapProperties) Coq(FSetPositive FMapPositive)