proposition: Lemma add_nodefault : forall l (Hd:NoDefault l) (Hs:Sorted (Raw.ltk key_ord) l) x e, NoDefault (raw_add_nodefault x e l).
proof: Proof. intros l Hd Hs x e. unfold raw_add_nodefault. case_eq (cmp e default_value); intro H; auto. - case_eq (Raw.mem key_comp x l); intro H0; auto. apply remove_nodefault; auto. - unfold NoDefault; intros k. assert (H0: e <> default_value). { intro H1. subst e. rewrite cmp_refl in H. discriminate. } destruct (eq_dec k x) as [e0|n]. + symmetry in e0. apply (Raw.add_1 key_comp l e) in e0. unfold not; intro. specialize (Raw.add_sorted key_comp Hs x e). intro Hsadd. specialize (Raw.MapsTo_inj Hsadd e0 H1). intro. contradiction. + unfold not; intro. assert (x <> k). unfold not in *. intro. apply n. symmetry; auto. specialize (Raw.add_3 key_comp l e H2 H1). intro. now apply Hd in H3. Qed.
imports: Bool OrderedType SMT_classes ProofIrrelevance