proposition: Lemma is_cocone_cocone_pushdown : forall f c, is_cocone c -> Functor.axioms f -> source f = cocone_target c -> is_cocone (cocone_pushdown f c).
proof: Proof. ir. uhg; ee. uf cocone_pushdown. ap cocone_like_cocone_create. rw coedge_nt_cocone_pushdown. app htrans_left_axioms. uh H; ee. am. rww otarget_coedge_nt. rw cocone_target_cocone_pushdown. rw vertex_cocone_pushdown. app ob_fob. rw H1. uh H; ee; am. rw coedge_nt_cocone_pushdown. rw target_htrans_left. rw target_coedge_nt. rw fcompose_right_constant_functor. rw cocone_source_cocone_pushdown. rw cocone_target_cocone_pushdown. rw vertex_cocone_pushdown. tv. am. am. app cocone_source_axioms. app ob_vertex. am. Qed.
imports: Arith limits