proposition: Lemma sort_cons_key p (l : klist elt) : sort O.ltk (p::l) <-> sort O.ltk l /\ [p] < l.
proof: Proof. rewrite (sort_app_key [p] l). firstorder. Qed.
imports: Coq(Bool BinPos Pnat Setoid SetoidList PeanoNat) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)