proposition: Lemma coedge_cocone_pushdown : forall f c x, ob (cocone_source c) x -> is_cocone c -> coedge (cocone_pushdown f c) x = fmor f (coedge c x).
proof: Proof. ir. uf coedge. rw coedge_nt_cocone_pushdown. rw ntrans_htrans_left. tv. rww osource_coedge_nt. Qed.
imports: Arith limits