proposition: Lemma is_iso_pre {D : precategory} {x y z : D} (f : x --> y) (g : y --> z) (H1 : is_iso (f · g)) (H2 : is_iso g) : is_iso f.
proof: Proof. set (iso1 := make_iso _ H1). set (iso2 := make_iso _ H2). set (inv1 := inv_from_iso iso1). set (inv2 := inv_from_iso iso2). use is_iso_qinv. - exact (g · inv1). - split. + rewrite assoc. unfold inv1. set (tmp := iso_inv_after_iso iso1). cbn in tmp. apply tmp. + set (tmp := iso_inv_after_iso iso2). cbn in tmp. rewrite <- tmp. clear tmp. rewrite <- assoc. apply cancel_precomposition. apply (post_comp_with_iso_is_inj _ _ g H2). set (tmp := iso_after_iso_inv iso2). cbn in tmp. rewrite tmp. clear tmp. rewrite <- assoc. set (tmp := iso_after_iso_inv iso1). cbn in tmp. exact tmp. Qed.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors