proposition: Lemma sort_app_key (l l' : klist elt) : sort O.ltk (l++l') <-> sort O.ltk l /\ sort O.ltk l' /\ l < l'.
proof: Proof. apply SortA_app_iff with (eqA:=O.eqk)(ltA:=O.ltk); ok. Qed.
imports: Coq(Bool BinPos Pnat Setoid SetoidList PeanoNat) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)