proposition: Lemma invertible_codotted_is_colimit : forall a, is_cocone a -> has_colimit (cosocle a) -> invertible (cocone_target a) (codotted a) -> is_colimit a.
proof: Proof. ir. assert (a = cocone_compose (codotted a) (colimit (cosocle a)) ). rww cocone_compose_codotted. rw H2. app is_colimit_cocone_compose. app is_colimit_colimit. app cocone_composable_codotted. rw cocone_target_colimit. rw target_cosocle. am. am. Qed.
imports: Arith limits