proposition: Lemma coedge_cocone_transform : forall c u x, cocone_transformable c u -> ob (cocone_source c) x -> coedge (cocone_transform c u) x = comp (cocone_target c) (coedge c x) (ntrans u x).
proof: Proof. ir. uf coedge. rw coedge_nt_cocone_transform. rw ntrans_vcompose. rw otarget_coedge_nt. tv. uh H; ee; am. uh H; ee. wr source_target. rw H2. rw source_cosocle. am. am. Qed.
imports: Arith limits