Mechanization of a Proof of String-Preprocessing in Boyer-Moore's Pattern Matching Algorithm