proposition: Lemma cocone_compose_id : forall c, is_cocone c -> cocone_compose (id (cocone_target c) (vertex c)) c = c.
proof: Proof. ir. ap cocone_extensionality. app is_cocone_cocone_compose. uhg; ee. am. ap mor_id. ap ob_vertex. am. rww source_id. app ob_vertex. am. rww vertex_cocone_compose. rww target_id. app ob_vertex. rww cosocle_cocone_compose. ir. rwi cocone_source_cocone_compose H0. rww coedge_cocone_compose. rww left_id. app ob_vertex. app mor_coedge. rww target_coedge. Qed.
imports: Arith limits