proposition: Lemma coedge_cocone_compose : forall c u x, ob (cocone_source c) x -> coedge (cocone_compose u c) x = comp (cocone_target c) u (coedge c x).
proof: Proof. ir. uf coedge. rw coedge_nt_cocone_compose. rw ntrans_vcompose. rw otarget_constant_nt. rw ntrans_constant_nt. tv. am. rw osource_coedge_nt. am. Qed.
imports: Arith limits