proposition: Lemma eq_num_dec: forall (n m: num), {n=m} + {n<>m}.
proof: Proof. intros n m. case_eq (eqb n m); intro H. rewrite eqb_true in H. auto. rewrite eqb_false in H. auto. Qed.
imports: ATBR(Common) ATBR(BoolView) ATBR(MyFSets MyFSetProperties MyFMapProperties) Coq(FSetPositive FMapPositive)