proposition: Lemma codotted_cocone_compose : forall u a, cocone_composable u a -> has_colimit (cosocle a) -> codotted (cocone_compose u a) = comp (cocone_target a) u (codotted a).
proof: Proof. ir. uf codotted. rw colimit_to_cocone_cocone_compose. rw cosocle_cocone_compose. rw cocone_target_colimit. rw target_cosocle. reflexivity. am. app is_colimit_colimit. rw cosocle_cocone_compose. am. am. rw cosocle_colimit. rw cosocle_cocone_compose. tv. rww cosocle_cocone_compose. Qed.
imports: Arith limits