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