magma-1518-obstruction-lean: Proposition A″ re-derives an observation of Bruno Le Floch

The write-up in magma-1518-obstruction-lean now says where Proposition A″ comes from: its equivalence of the four single-variable targets 47, 614, 817 and 3862 under 1518 together with left injectivity and left surjectivity — which hold in every finite 1518-magma — re-derives an observation of Bruno Le Floch posted on the Lean Zulip’s Equational stream in October 2025, that in a finite 1518-magma the squaring map and all left multiplications are bijective and the single-variable targets are then equivalent to each other and to S S S x = x. Naming the observation that was being re-derived is the difference between a proposition that stands on its own and one that stands on someone else’s step.