proposition: Lemma lt_spec : forall n m, reflect (lt n m) (ltb n m).
proof: Proof. intros n m; unfold ltb. case_eq (Pos.compare n m); intro H; try constructor. intro H'. apply Pcompare_Eq_eq in H. subst. refine (Pos.lt_irrefl _ H'). auto. intro H'. apply ZC1 in H. assert (H'' := Pos.lt_trans _ _ _ H H'). refine (Pos.lt_irrefl _ H''). Qed.
imports: ATBR(Common) ATBR(BoolView) ATBR(MyFSets MyFSetProperties MyFMapProperties) Coq(FSetPositive FMapPositive)