Impossibility of the Dissection of a Cube

This entry formalizes Littlewood's argument, demonstrating that a 3-dimensional cube cannot be dissected into a finite collection of smaller cubes, each of a different size. The formalization addresses theorem #82, "Dissection of Cubes (J.E. Littlewood's 'elegant' proof)" from Freek Wiedijk's "100 Mathematical Theorems" list, and is based upon a prior formalization in Lean.