proposition: Lemma leb_true : forall x y, leb x y = true <-> le x y.
proof: Proof. intros. case le_spec; intuition discriminate. Qed.
imports: ATBR(Common) ATBR(BoolView) ATBR(MyFSets MyFSetProperties MyFMapProperties) Coq(FSetPositive FMapPositive)