proposition: Lemma ApartL_appr lA lB lB' : lA < lB++lB' <-> lA < lB /\ lA < lB'.
proof: Proof. unfold "<", lt_klist. setoid_rewrite in_app_iff; firstorder. Qed.
imports: Coq(Bool BinPos Pnat Setoid SetoidList PeanoNat) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)