proposition: Lemma le_spec : forall n m, reflect (le n m) (leb n m).
proof: Proof. intros n m; unfold leb. case_eq (Pos.compare n m); intro H; try constructor. apply Pcompare_Eq_eq in H. subst. unfold le,Pos.le,Pos.compare. rewrite Pcompare_refl. intro; discriminate. unfold le. unfold Pos.le. rewrite H. intro; discriminate. apply ZC1 in H. unfold le, Pos.le. apply ZC2 in H. rewrite H. intro. tauto_false. Qed.
imports: ATBR(Common) ATBR(BoolView) ATBR(MyFSets MyFSetProperties MyFMapProperties) Coq(FSetPositive FMapPositive)