Still obsessed with this problem, but making fantastic progress today. TeXed up about four pages of lemmas (and a statement of the goal) that actually hang together and get me about 75% of the way towards the result I think. It is, of course, always the last 25% (or 5%, or 1%) that gets me, but the mental exercise of futzing around all these inductive hypotheses is awfully fun.
Though, hm... it was the case a couple of days ago that I had a conjecture whose proof had 12 cases, and by chance the single case that was false was the very last one I tried. I really should stop getting so prematurely optimistic.
Though, hm... it was the case a couple of days ago that I had a conjecture whose proof had 12 cases, and by chance the single case that was false was the very last one I tried. I really should stop getting so prematurely optimistic.