proposition: Lemma comp_coedge_colimit_to_cocone : forall r s x b, is_colimit s -> is_cocone r -> cosocle r = cosocle s -> b = cocone_target s -> ob (cocone_source s) x -> comp b (colimit_to_cocone s r) (coedge s x) = coedge r x.
proof: Proof. ir. rw H2. transitivity (coedge (cocone_compose (colimit_to_cocone s r) s) x). rww coedge_cocone_compose. rw cocone_compose_colimit_to_cocone. tv. am. am. am. Qed.
imports: Arith limits