proposition: Lemma cancel_z_iso {M : precategory} {x y z : M} (f f' : x --> y) (g : z_iso y z) : f · g = f' · g -> f = f'.
proof: Proof. intro e. destruct g as [g [g' H]]. apply (post_comp_with_z_iso_is_inj H). assumption. Qed.
imports: UniMath.Foundations.PartA UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Categories