Proof of `Cancellation outside double covers in higher moments` (2nd statement)
groundedproofs/Lax253009Proofs/HigherMoments.lean · lax-253009
What this proof establishes
no assumptions
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
Choose two distinct covering positions for each point, take their union, and enlarge this selection to the requested cardinality. This extracts the double subcover used in Lemma 4.16.