proposition: Lemma ApartL_rev lA lB : (rev lA) < lB <-> lA < lB.
proof: Proof. unfold "<", lt_klist. now setoid_rewrite <- in_rev. Qed.
imports: Coq(Bool BinPos Pnat Setoid SetoidList PeanoNat) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)