fact: Fixpoint rev_append (y x : positive) : positive := match y with | 1 => x | y~1 => rev_append y x~1 | y~0 => rev_append y x~0 end.
imports: Coq(Bool PeanoNat BinPos Orders OrdersEx OrdersLists) MMaps(Utils Comparisons Interface)