proposition: Lemma Inv_iso_unique : forall f g : Iso, Iso_mor f =_S Iso_mor g -> Inv_iso f =_S Inv_iso g.
proof: Proof. intros f g H. apply Trans with ((Inv_iso f o Iso_mor f) o Inv_iso g). apply Trans with (Inv_iso f o Iso_mor f o Inv_iso g). apply Trans with (Inv_iso f o Id a). apply Idr. apply Comp_l. apply Trans with (Iso_mor g o Inv_iso g). apply Sym; apply (Idr_inv g). apply Comp_r; apply Sym; trivial. apply Ass. apply Trans with (Id b o Inv_iso g). apply Comp_r; apply (Idl_inv f). apply Idl. Qed.
imports: Dual