proposition: Lemma edge_cone_compose : forall c u x, ob (cone_source c) x -> cone_composable c u -> edge (cone_compose c u) x = comp (cone_target c) (edge c x) u.
proof: Proof. ir. uf edge. rw edge_nt_cone_compose. rw ntrans_vcompose. rw otarget_edge_nt. ap uneq. rw ntrans_constant_nt. tv. am. rw osource_constant_nt. am. Qed.
imports: Arith nat_trans