proposition: Lemma search_add : forall T (r:hashtools T) (s t:T)(u:hashtable T), (tools_ok r) -> search r s (add r t u) = bool_or (comp r s t) (search r s u).
proof: Proof. intros. unfold search. pose (p:= pos_compare (addr r s) (addr r t)). induction (bool_alt p). rewrite get_add_same. rewrite check_cons. reflexivity. assumption. rewrite get_add_diff. assert (comp r s t = false). unfold tools_ok in H. induction (bool_alt (comp r s t)). unfold p in H0. rewrite (H _ _ H1) in H0. rewrite pos_compare_refl in H0. discriminate H0. assumption. rewrite H1. reflexivity. assumption. Qed.