proposition: Lemma raw_add_d_rem : forall m (Hm: Sorted (Raw.ltk key_ord) m) x, raw_add_nodefault x default_value m = Raw.remove key_comp x m.
proof: Proof. intros m Hm x. unfold raw_add_nodefault. rewrite cmp_refl. case_eq (Raw.mem key_comp x m); intro H; 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 k. destruct (eq_dec x k) as [e|n]. - subst. split. + intro. contradiction. + intro. contradict H0. apply Raw.remove_1; auto. - apply Raw.remove_4; auto. } * { intros k e e' H0 H1. destruct (eq_dec x k) as [e0|n]. - assert (H2: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 H2. specialize (Raw.MapsTo_inj H2 H0 H1). intro H3. subst. apply cmp_refl. } Qed.
imports: Bool OrderedType SMT_classes ProofIrrelevance