proposition: Lemma cone_compose_cone_transform : forall f c u, is_cone c -> cone_composable c u -> cone_transformable f c -> cone_compose (cone_transform f c) u = cone_transform f (cone_compose c u).
proof: Proof. ir. ap cone_extensionality. rww is_cone_cone_compose. uhg; ee. app is_cone_cone_transform. rww cone_target_cone_transform. lu. rww vertex_cone_transform. lu. app is_cone_cone_transform. uhg; ee. rww is_cone_cone_compose. lu. rw socle_cone_compose. lu. rw vertex_cone_compose; rww vertex_cone_transform. rww vertex_cone_compose. rw socle_cone_compose. rww socle_cone_transform. rww socle_cone_transform. ir. rwi cone_source_cone_compose H2. rwi cone_source_cone_transform H2; try am. assert (osource f = cone_source c). uf cone_source. uf osource. ap uneq; lu. assert (otarget f = cone_target c). uf cone_target. wr target_source. ap uneq. uh H1; ee. am. lu. rw edge_cone_compose. rw edge_cone_transform. rw edge_cone_transform. rww cone_target_cone_transform. rww cone_target_cone_compose. rww edge_cone_compose. rww assoc. app mor_ntrans. lu. uh H1; ee. rww H3. sy; am. app mor_edge. uh H0; ee. am. rww source_ntrans. rww target_edge. uh H1; ee. rww H6. lu. rww H3. rww source_edge. sy; lu. rww H3. uhg; ee. rww is_cone_cone_compose. lu. rww socle_cone_compose. lu. rww H3. am. rww cone_source_cone_transform. uhg; ee. app is_cone_cone_transform. rww cone_target_cone_transform. uh H0; ee; am. rww vertex_cone_transform. lu. Qed.
imports: Arith nat_trans