proposition: Lemma cocone_compose_cocone_transform : forall f c u, is_cocone c -> cocone_composable u c -> cocone_transformable c f -> cocone_compose u (cocone_transform c f) = cocone_transform (cocone_compose u c) f.
proof: Proof. ir. ap cocone_extensionality. app is_cocone_cocone_compose. uhg; ee. app is_cocone_cocone_transform. rww cocone_target_cocone_transform. lu. rww vertex_cocone_transform. lu. app is_cocone_cocone_transform. uhg; ee. app is_cocone_cocone_compose. lu. rw cosocle_cocone_compose. lu. rw vertex_cocone_compose; rww vertex_cocone_transform. rww vertex_cocone_compose. rw cosocle_cocone_compose. rww cosocle_cocone_transform. rww cosocle_cocone_transform. ir. rwi cocone_source_cocone_compose H2. rwi cocone_source_cocone_transform H2; try am. assert (osource f = cocone_source c). uf cocone_source. wr source_target. ap uneq. uh H1; ee. am. uh H1; ee; am. assert (otarget f = cocone_target c). uf cocone_target. uf otarget. ap uneq. uh H1; ee; am. rw coedge_cocone_compose. rw coedge_cocone_transform. rw coedge_cocone_transform. rww cocone_target_cocone_transform. rww cocone_target_cocone_compose. rww coedge_cocone_compose. rww assoc. uh H0; ee; am. app mor_coedge. uh H0; ee. ap mor_ntrans. uh H1; ee; am. rww H3. sy; am. rww target_coedge. uh H0; ee; am. rw target_ntrans. rw source_coedge. uh H1; ee. rww H6. am. am. uh H1; ee; am. rww H3. uhg; ee. app is_cocone_cocone_compose. lu. rww cosocle_cocone_compose. lu. rw cocone_source_cocone_compose. am. am. am. rww cocone_source_cocone_transform. Qed.
imports: Arith limits