proposition: Lemma iso_inv_on_left {C : precategory} (a b c : ob C) (f : a --> b) (g : iso b c) (h : a --> c) (H : h = f · g) : f = h · inv_from_iso g.
proof: Proof. assert (H2 : h · inv_from_iso g = (f · g) · inv_from_iso g). rewrite H. apply idpath. rewrite <- assoc in H2. rewrite iso_inv_after_iso in H2. rewrite id_right in H2. apply pathsinv0. assumption. Qed.
imports: UniMath.Foundations.PartA UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Categories