Weird. It's not my field at all but intuitively, I would have approached a proof by trying to formalise the following:
1/ Complete part of the tiling in the upper right quadrant (this tiling exists by assumption)
2/ Shove all the tiles down and to the left
3/ Repeat.
It's very surprising that step 2 needs the axiom of choice. (Usually when I'm this surprised it means I've misunderstood something!)
Edit: your link proves something stronger - that the ability to tile an nxn square for all n is equivalent to tiling a quadrant and tiling a plane. I guess that's where choice comes in, is it?
1/ Complete part of the tiling in the upper right quadrant (this tiling exists by assumption)
2/ Shove all the tiles down and to the left
3/ Repeat.
It's very surprising that step 2 needs the axiom of choice. (Usually when I'm this surprised it means I've misunderstood something!)
Edit: your link proves something stronger - that the ability to tile an nxn square for all n is equivalent to tiling a quadrant and tiling a plane. I guess that's where choice comes in, is it?