proposition: Lemma cone_pushdown_cone_compose : cone_pushdown f (cone_compose a u) = cone_compose (cone_pushdown f a) (fmor f u).
proof: Proof. ap cone_extensionality. ap is_cone_cone_pushdown. rww is_cone_cone_compose. ap cone_composable_a_u. am. rww cone_target_cone_compose. rww is_cone_cone_compose. uhg; ee. app is_cone_cone_pushdown. rww cone_target_cone_pushdown. app mor_fmor. rww target_fmor. rww vertex_cone_pushdown. rww K3. rww vertex_cone_pushdown. rww vertex_cone_compose. rww vertex_cone_compose. rww source_fmor. rww socle_cone_pushdown. rww socle_cone_compose. rww socle_cone_compose. rww socle_cone_pushdown. ir. rwi cone_source_cone_pushdown H. rwi cone_source_cone_compose H. rw edge_cone_pushdown. rw edge_cone_compose. rw edge_cone_compose. rw cone_target_cone_pushdown. rw edge_cone_pushdown. wr K1. wr comp_fmor. tv. am. rw K1. app mor_edge. rww K1. wrr K1. rww source_edge. sy; am. am. am. rww cone_source_cone_pushdown. uhg; ee. app is_cone_cone_pushdown. rww cone_target_cone_pushdown. app mor_fmor. rww vertex_cone_pushdown. rww target_fmor. rww K3. am. ap cone_composable_a_u. rww cone_source_cone_compose. rww is_cone_cone_compose. ap cone_composable_a_u. Qed.
imports: Arith nat_trans