proposition: Proposition iso_sym_right_inverse {C : Category} {x y : C} (f : x ≅ y) : iso_compose f (iso_sym f) ≈ iso_id.
proof: Proof. apply to_equiv_implies_iso_equiv, iso_to_from. Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Morphisms