proposition: Lemma edge_cone_transform : forall u c x, ob (osource u) x -> cone_transformable u c -> edge (cone_transform u c) x = comp (cone_target c) (ntrans u x) (edge c x).
proof: Proof. ir. uf edge. rw edge_nt_cone_transform. rw ntrans_vcompose. uh H0; ee. wr target_source. rw H2. tv. am. uh H0. ee. rw osource_edge_nt. uf cone_source. wr H2. am. am. Qed.
imports: Arith nat_trans