So the "kindergarten obvious" statement is: "For all natural numbers x and y, if 3x = 3y, then x = y" An equally trivial but rather more abstract way to phras

So the "kindergarten obvious" statement is: "For all natural numbers x and y, if 3x = 3y, then x = y" An equally trivial but rather more abstract way to phrase this is in the category of finite sets: "For all finite sets x and y, whenever there's a bijection between the product x cross 3 and the product y cross 3, then there's a bijection between x and y". (Here "3" represents any set of cardinality 3, but typically chosen to be the set {0,1,2} where 0 = {}, 1 = {0}, 2 = {0,1}). What's (apparently!) not so trivial, is when you remove the "finite" restriction from the above, and you want to show it holds for all sets, including those of various infinite cardinalities. Actually constructing the bijection seems like it would require an infinite number of arbitrary choices, which is why it's impressive they don't rely on the axiom of choice.