proposition: Lemma coedge_nt_cocone_compose : forall u c, coedge_nt (cocone_compose u c) = (vcompose (constant_nt (cocone_source c) (cocone_target c) u) (coedge_nt c)).
proof: Proof. ir. uf cocone_compose. rw coedge_nt_cocone_create. tv. Qed.
imports: Arith limits