proposition: Lemma z_iso_two_of_three_left {C : category} {x y z : C} {f : x --> y} {g : y --> z} (gf_is_iso : is_z_isomorphism (f · g)) (g_is_iso : is_z_isomorphism g) : is_z_isomorphism f.
proof: Proof. apply is_z_iso_from_is_iso. eapply iso_two_of_three_left. exact (is_iso_from_is_z_iso _ gf_is_iso). exact (is_iso_from_is_z_iso _ g_is_iso). Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Monics UniMath.CategoryTheory.Epis UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Isos