proposition: Lemma raw_add_d_rem : forall m (Hm: Sorted (Raw.ltk key_ord) m) x d, raw_add_nodefault x d d m = Raw.remove key_comp x m.
proof: Proof. intros. unfold raw_add_nodefault. rewrite cmp_refl. case_eq (Raw.mem key_comp x m); intro. auto. apply Raw.mem_3 in H; auto. apply raw_equal_eq; auto. apply Raw.remove_sorted; auto. apply Raw.equal_1; auto. apply Raw.remove_sorted; auto. unfold Raw.Equivb. split. intros. destruct (eq_dec x k). subst. split. intro. contradiction. intro. contradict H0. apply Raw.remove_1; auto. apply Raw.remove_4; auto. intros. destruct (eq_dec x k). assert (exists e, InA (Raw.eqk (elt:=elt)) (k, e) (Raw.remove key_comp x m)). exists e'. apply Raw.InA_eqke_eqk; auto. rewrite <- Raw.In_alt in H2; auto. contradict H2. apply Raw.remove_1; auto. apply key_comp. apply (Raw.remove_2 key_comp Hm n) in H0. specialize (Raw.remove_sorted key_comp Hm x). intros. specialize (Raw.MapsTo_inj key_dec H2 H0 H1). intro. subst. apply cmp_refl. Qed.
imports: Bool OrderedType SMT_classes ProofIrrelevance