proposition: Lemma cone_compose_cone_compose : forall a u v, cone_composable a u -> composable (cone_target a) u v -> cone_compose (cone_compose a u) v = cone_compose a (comp (cone_target a) u v).
proof: Proof. ir. rwi composable_facts_rw H0. apply cone_extensionality. rww is_cone_cone_compose. uf cone_composable; ee. rww is_cone_cone_compose. rw cone_target_cone_compose. lu. rw vertex_cone_compose. sy; lu. rww is_cone_cone_compose. uhg; ee. lu. rww mor_comp. lu. lu. lu. rw target_comp. lu. lu. lu. lu. rw vertex_cone_compose. rw vertex_cone_compose. rw source_comp. tv. lu. lu. lu. rw socle_cone_compose. rw socle_cone_compose. rw socle_cone_compose. tv. ir. rw edge_cone_compose. rw cone_target_cone_compose. rw edge_cone_compose. rw edge_cone_compose. rw assoc. tv. ap mor_edge. rwi cone_source_cone_compose H1. rwi cone_source_cone_compose H1. am. lu. uh H; ee. am. uh H0; ee; am. rw source_edge. sy; lu. rwi cone_source_cone_compose H1. rwi cone_source_cone_compose H1. am. lu. lu. tv. rwi cone_source_cone_compose H1. rwi cone_source_cone_compose H1. am. uhg; ee. lu. rww mor_comp. uh H0; ee; am. uh H0; ee; am. lu. rw target_comp. lu. uh H0; ee; am. uh H0; ee; am. lu. rwi cone_source_cone_compose H1. rwi cone_source_cone_compose H1. am. am. rw cone_source_cone_compose. rwi cone_source_cone_compose H1. rwi cone_source_cone_compose H1. am. uhg; ee. rww is_cone_cone_compose. rw cone_target_cone_compose. uh H0; ee; am. rw vertex_cone_compose. sy; lu. Qed.
imports: Arith nat_trans