Resolution theorem for K0 in Lean/Mathlib: induction on hasFiniteResolutionOfLength without horseshoe

Mathlib has ObjectProperty.hasFiniteResolutionOfLength P n (inductive: R0 = P, X in R(n+1) via 0->K->E->X->0, E in P, K in Rn) and hasFiniteResolution. To prove K0(P) = K0(P.hasFiniteResolution) (P closed under extensions + kernels of epis, every object a quotient of a P-object), prove by ONE induction: (a) Rn closed under extensions, (b) Schanuel: 0->K->A->X->0 with A in Rn, X in R(n+1) gives K in Rn. (a)n => (b)n: pull a resolution of X back along A->X with ShortComplex.ShortExact.pull (both orders; pullbackSymmetry to match objects). (b)n => (a)(n+1): cover the middle term by F in P, apply (b) to F->X'' and then to 0->ker(F->X)->ker(F->X'')->X'->0. Then apply a one-step theorem to Rn <= R(n+1) and glue: any SES lies in a single R_N with N = max.