proposition: Proposition from_equiv_implies_iso_equiv {C : Category} {x y} (f g : x ≅ y) : from f ≈ from g -> f ≈ g.
proof: Proof. set (f1 := iso_sym f). set (g1 := iso_sym g). change f with (iso_sym (iso_sym f)). change g with (iso_sym (iso_sym g)). change (iso_sym f) with f1. change (iso_sym g) with g1. clearbody f1 g1. clear f g. simpl. intro eq; apply to_equiv_implies_iso_equiv in eq. now apply iso_sym_proper. Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Morphisms