Proof of `Basic properties of Sprague–Grundy values` (1st statement)
groundedproofs/Lax689614Proofs/DisjointUnion.lean · lax-689614
What this proof establishes
Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.
Description
Induct on the total number of vertices. Each move changes one component. The xor of the two values is unreachable, while every smaller value is reachable by the xor comparison lemma and the mex property.