proposition: Lemma colimit_to_cocone_invertible_is_colimit : forall a b, is_colimit b -> is_cocone a -> cosocle a = cosocle b -> invertible (cocone_target b) (colimit_to_cocone b a) -> is_colimit a.
proof: Proof. ir. assert (a = cocone_compose (colimit_to_cocone b a) b). rw cocone_compose_colimit_to_cocone. tv. am. am. am. rw H3. ap is_colimit_cocone_compose. am. uhg; ee. uh H; ee. uh H; ee; am. app mor_colimit_to_cocone. rww source_colimit_to_cocone. lu. Qed.
imports: Arith limits