Er, nevermind. Misread the invariant as mismatches > 0 and couldn't understand why there couldn't be 0 mismatches.