proposition: Lemma colimit_to_cocone_cocone_compose : forall a b u, is_colimit b -> cocone_composable u a -> cosocle a = cosocle b -> colimit_to_cocone b (cocone_compose u a) = comp (cocone_target b) u (colimit_to_cocone b a).
proof: Proof. ir. set (k:= comp (cocone_target b) u (colimit_to_cocone b a)). assert (cocone_target a = cocone_target b). uf cocone_target. rww H1. assert (lem1 : is_cocone a). lu. transitivity (colimit_to_cocone b (cocone_compose k b)). uf k. wr cocone_compose_cocone_compose. rw cocone_compose_colimit_to_cocone. tv. lu. am. am. app cocone_composable_colimit_to_cocone. app show_composable. wr H2; uh H0; ee; am. app mor_colimit_to_cocone. rww target_colimit_to_cocone. uh H0; ee; am. rww colimit_to_cocone_cocone_compose1. uf k. uhg; ee. uh H; ee. uh H; ee; am. rww mor_comp. wr H2; uh H0; ee; am. app mor_colimit_to_cocone. rww target_colimit_to_cocone. uh H0; ee; am. rw source_comp. rww source_colimit_to_cocone. wr H2; uh H0; ee; am. app mor_colimit_to_cocone. rww target_colimit_to_cocone. uh H0; ee; am. Qed.
imports: Arith limits