proposition: Lemma inv_from_iso_comp {D : precategory} {x y z : D} (f : iso x y) (g : iso y z) : inv_from_iso (iso_comp f g) = inv_from_iso g · inv_from_iso f.
proof: Proof. apply pathsinv0. apply inv_iso_unique'. unfold precomp_with. unfold iso_comp. cbn. rewrite assoc. rewrite <- (assoc _ g). rewrite iso_inv_after_iso. rewrite id_right. apply iso_inv_after_iso. Qed.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors