proposition: Lemma cocone_pushdown_cocone_compose : cocone_pushdown f (cocone_compose u a) = cocone_compose (fmor f u) (cocone_pushdown f a).
proof: Proof. ap cocone_extensionality. ap is_cocone_cocone_pushdown. app is_cocone_cocone_compose. ap cocone_composable_u_a. am. rww cocone_target_cocone_compose. app is_cocone_cocone_compose. uhg; ee. app is_cocone_cocone_pushdown. rww cocone_target_cocone_pushdown. app mor_fmor. rww source_fmor. rww vertex_cocone_pushdown. rww K3. rww vertex_cocone_pushdown. rww vertex_cocone_compose. rww vertex_cocone_compose. rww target_fmor. rww cosocle_cocone_pushdown. rww cosocle_cocone_compose. rww cosocle_cocone_compose. rww cosocle_cocone_pushdown. ir. rwi cocone_source_cocone_pushdown H. rwi cocone_source_cocone_compose H. rw coedge_cocone_pushdown. rw coedge_cocone_compose. rw coedge_cocone_compose. rw cocone_target_cocone_pushdown. rw coedge_cocone_pushdown. wr K1. wr comp_fmor. tv. am. am. rw K1. app mor_coedge. rww target_coedge. am. am. rww cocone_source_cocone_pushdown. uhg; ee. app cocone_source_axioms. app ob_is_ob. rww cocone_source_cocone_compose. app is_cocone_cocone_compose. uhg; ee; try am. wrr K1. Qed.
imports: Arith limits