proposition: Lemma is_cocone_cocone_compose : forall c u, cocone_composable u c -> is_cocone (cocone_compose u c).
proof: Proof. ir. assert (is_cocone c). lu. uhg; ee. uf cocone_like. uf cocone_compose. rw vertex_cocone_create. rw coedge_nt_cocone_create. tv. rw coedge_nt_cocone_compose. rww vcompose_axioms. ap constant_nt_axioms. app cocone_source_axioms. app cocone_target_axioms. uh H; ee; am. app coedge_nt_axioms. rww source_constant_nt. rw target_coedge_nt. uh H; ee. rww H2. am. rw cocone_target_cocone_compose. rw vertex_cocone_compose. rw ob_target. tv. uh H; ee; am. rw coedge_nt_cocone_compose. rw target_vcompose. rw target_constant_nt. rw cocone_source_cocone_compose. rw cocone_target_cocone_compose. rw vertex_cocone_compose. tv. Qed.
imports: Arith limits