proposition: Lemma coedge_cocone_pullback : forall f c x, ob (source f) x -> coedge (cocone_pullback f c) x = coedge c (fob f x).
proof: Proof. ir. uf coedge. rw coedge_nt_cocone_pullback. rw ntrans_htrans_right. tv. am. Qed.
imports: Arith limits