fact: Definition K_0_class {M:ExactCategory} : ob M -> K_0 M := λ A, @presented_abgr_intro (π₀ M) _ (pi0pr _ A).
imports: UniMath.Tactics.EnsureStructuredProofs UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.ExactCategories.ExactCategories UniMath.Algebra.Groups UniMath.Algebra.Free_Monoids_and_Groups