proposition: Lemma is_cone_cone_compose : forall c u, cone_composable c u -> is_cone (cone_compose c u) = True.
proof: Proof. ir. ap iff_eq; ir; try tv. uhg; ee. uf cone_like. uf cone_compose. rw vertex_cone_create. rw edge_nt_cone_create. tv. rw edge_nt_cone_compose. rww vcompose_axioms. lu. ap constant_nt_axioms. ap cone_source_axioms. lu. ap cone_target_axioms. lu. lu. rw target_constant_nt. uh H; ee. uh H; ee. rw H2; am. rw cone_target_cone_compose. rw vertex_cone_compose. uh H; ee. rww ob_source. rw edge_nt_cone_compose. rw source_vcompose. rw source_constant_nt. rw cone_source_cone_compose. rw cone_target_cone_compose. rw vertex_cone_compose. tv. Qed.
imports: Arith nat_trans