proposition: Lemma cocone_compose_cocone_compose : forall a u v, cocone_composable u a -> composable (cocone_target a) v u -> cocone_compose v (cocone_compose u a) = cocone_compose (comp (cocone_target a) v u) a.
proof: Proof. ir. rwi composable_facts_rw H0. apply cocone_extensionality. app is_cocone_cocone_compose. uf cocone_composable; ee. app is_cocone_cocone_compose. rw cocone_target_cocone_compose. lu. rw vertex_cocone_compose. uh H0; ee; am. app is_cocone_cocone_compose. uhg; ee. lu. rww mor_comp. lu. lu. lu. rw source_comp. lu. lu. lu. lu. rw vertex_cocone_compose. rw vertex_cocone_compose. rw target_comp. tv. lu. lu. lu. rw cosocle_cocone_compose. rw cosocle_cocone_compose. rw cosocle_cocone_compose. tv. ir. rw coedge_cocone_compose. rw cocone_target_cocone_compose. rw coedge_cocone_compose. rw coedge_cocone_compose. rw assoc. tv. uh H0; ee; am. uh H0; ee; am. ap mor_coedge. rwi cocone_source_cocone_compose H1. rwi cocone_source_cocone_compose H1. am. lu. uh H; ee. uh H0; ee; am. rw target_coedge. uh H; ee; am. rwi cocone_source_cocone_compose H1. rwi cocone_source_cocone_compose H1. am. lu. tv. rwi cocone_source_cocone_compose H1. rwi cocone_source_cocone_compose H1. am. uhg; ee. ap cocone_source_axioms. lu. ap ob_is_ob. rwi cocone_source_cocone_compose H1. rwi cocone_source_cocone_compose H1. am. rwi cocone_source_cocone_compose H1. am. Qed.
imports: Arith limits