In class you proved that any full n x m board is a winning configuration (provided it has at least two squares).
Indeed, the proof was existential - it did not involve finding the winning strategy. Some proofs are like that.
This does not mean that you cannot compute the winning strategy itself. As you noted, the function win() implicitly looks for a winning strategy, and could in principle print one if it found it (the current code does not print winning strategies, and the function simply returns whether such a strategy exists). Note, though, that win() performs an exhaustive search over all legal games; you can try to solve (almost) any problem using exhaustive searches, but the solution is often not tractable.