proposition: Lemma add_sorted : forall l d (Hs:Sorted (Raw.ltk key_ord) l) x e, Sorted (Raw.ltk key_ord) (raw_add_nodefault x e d l).
proof: Proof. intros. unfold raw_add_nodefault. case (cmp e d); auto. case (Raw.mem key_comp x l); auto. apply Raw.remove_sorted; auto. apply Raw.add_sorted; auto. Qed.
imports: Bool OrderedType SMT_classes ProofIrrelevance