proposition: Lemma colimit_to_cocone_cocone_compose1 : forall a u, is_colimit a -> cocone_composable u a -> colimit_to_cocone a (cocone_compose u a) = u.
proof: Proof. ir. assert (lem1 : is_colimit a). am. uh H; ee. uh H; ee. ap H2. uhg; ee. am. ap mor_colimit_to_cocone. app is_cocone_cocone_compose. am. rw cosocle_cocone_compose. tv. tv. rw source_colimit_to_cocone. tv. app is_cocone_cocone_compose. am. rw cosocle_cocone_compose. tv. am. rw cocone_compose_colimit_to_cocone. tv. app is_cocone_cocone_compose. am. rww cosocle_cocone_compose. Qed.
imports: Arith limits