proposition: Lemma is_cone_cone_transform : forall u c, cone_transformable u c -> is_cone (cone_transform u c).
proof: Proof. ir. uhg; ee. uf cone_transform. app cone_like_cone_create. rw edge_nt_cone_transform. rww vcompose_axioms. lu. uh H; ee. uh H; ee. am. uh H; ee. am. rw vertex_cone_transform. rww cone_target_cone_transform. uh H; ee. uh H; ee. am. rw edge_nt_cone_transform. rw source_vcompose. rw source_edge_nt. rw cone_source_cone_transform. rw cone_target_cone_transform. rww vertex_cone_transform. am. am. lu. Qed.
imports: Arith nat_trans