proposition: Lemma add_nodefault : forall l d (Hd:NoDefault l d) (Hs:Sorted (Raw.ltk key_ord) l) x e, NoDefault (raw_add_nodefault x e d l) d.
proof: Proof. intros. unfold raw_add_nodefault. case_eq (cmp e d); intro; auto. case_eq (Raw.mem key_comp x l); intro; auto. apply remove_nodefault; auto. unfold NoDefault; intros. assert (e <> d). unfold cmp in H. case (compare e d) in H; try now contradict H. apply lt_not_eq in l0; auto. apply lt_not_eq in l0; now auto. destruct (eq_dec k x). - symmetry in e0. apply (Raw.add_1 key_dec key_comp l e) in e0. unfold not; intro. specialize (Raw.add_sorted key_dec key_comp Hs x e). intro Hsadd. specialize (Raw.MapsTo_inj key_dec Hsadd e0 H1). intro. contradiction. - unfold not; intro. assert (x <> k). unfold not in *. intro. apply n. symmetry; auto. specialize (Raw.add_3 key_dec key_comp l e H2 H1). intro. now apply Hd in H3. Qed.
imports: Bool OrderedType SMT_classes ProofIrrelevance