proposition: Lemma cocone_composable_cocommutation : cocone_composable cocommutation b.
proof: Proof. uhg; ee. cp colimit_b. uh H; ee. lu. rw cocone_target_b. ap mor_cocommutation. rw source_cocommutation. tv. Qed.
imports: Arith limits