proposition: Lemma cocone_compose_cocommutation : cocone_compose cocommutation b = cocone_pushdown f a.
proof: Proof. uf cocommutation. rw cocone_compose_colimit_to_cocone. tv. app is_cocone_cocone_pushdown. am. rww cosocle_cocone_pushdown. Qed.
imports: Arith limits