proposition: Lemma mor_coedge : forall c x, ob (cocone_source c) x -> is_cocone c -> mor (cocone_target c) (coedge c x).
proof: Proof. ir. uf coedge. ap mor_ntrans. lu. rww osource_coedge_nt. rww otarget_coedge_nt. Qed.
imports: Arith limits