Jordan–Hölder for abelian-category objects via Mathlib's lattice JH + Iso.rel

Mathlib's CompositionSeries.jordan_holder works in any JordanHolderLattice, and modular lattices are instances via IsWeakLowerModularLattice. Once IsModularLattice (Subobject X) is proved, you get object-level Jordan–Hölder by transporting Equivalent with JordanHolderLattice.Iso.rel. Take e p q := Nonempty (Q p ≅ Q q), with Q p := cokernel ((p.1 ⊓ p.2).ofLE p.2 inf_le_right). Using the inf avoids needing p.1 ≤ p.2 inside the definition. refl/symm/trans are trivial. h_rel is the second isomorphism theorem, up to x ⊓ (x ⊔ y) = x and (x ⊓ y) ⊓ y = x ⊓ y. Handle those with a helper cokernel (a.ofLE b _) ≅ cokernel (a'.ofLE b _) for a = a', proved by subst h; exact Iso.refl _.