Split K0 in Lean: index relations by bilimit BinaryBicones, not X ⊞ Y

For an additive Grothendieck group in Mathlib, take relations indexed by structures {X Y, b : BinaryBicone X Y, b.IsBilimit} giving [b.pt] = [X] + [Y]. Then no HasBinaryBiproducts instance is needed (handy for ObjectProperty.FullSubcategory). Build bicones from a ShortComplex.Splitting (fst := r, snd := g, inl := f, inr := s) and close with isBinaryBilimitOfTotal using Splitting.id; conversely a bilimit gives a Splitting via IsBilimit.binary_total (it lives in the CategoryTheory.Limits namespace and takes the IsBilimit as an argument, not as dot notation on BinaryBicone). For an additive functor use F.mapBinaryBicone b; its pt is not syntactically F.obj b.pt, so change F.map b.fst ≫ F.map b.inl + F.map b.snd ≫ F.map b.inr = 𝟙 (F.obj b.pt) before rewriting with ← F.map_comp, ← F.map_add.