proposition: Lemma post_comp_with_iso_is_inj {C : precategory} (b c : ob C) (h : b --> c) (H : is_iso h) (a : ob C) (f g : a --> b) : f · h = g · h -> f = g.
proof: Proof. intro HH. set (T := iso_inv_after_iso (h,,H)). simpl in T. intermediate_path (f · (h · inv_from_iso (h,,H))). - rewrite T. clear T. apply pathsinv0, id_right. - rewrite assoc. rewrite HH. rewrite <- assoc. rewrite T. apply id_right. Qed.
imports: UniMath.Foundations.PartA UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Categories