proposition: Lemma is_cocone_cocone_transform : forall u c, cocone_transformable c u -> is_cocone (cocone_transform c u).
proof: Proof. ir. cp H; uh H; ee. uhg; ee. uf cocone_transform. app cocone_like_cocone_create. rw coedge_nt_cocone_transform. rww vcompose_axioms. app coedge_nt_axioms. rww source_coedge_nt. sy; am. rw vertex_cocone_transform. rww cocone_target_cocone_transform. uh H; ee. am. rw coedge_nt_cocone_transform. rw target_vcompose. rw target_coedge_nt. rw cocone_source_cocone_transform. rw cocone_target_cocone_transform. rww vertex_cocone_transform. am. am. am. Qed.
imports: Arith limits