proposition: Lemma colimit_to_cocone_pr : forall a b, is_cocone a -> is_colimit b -> cosocle a = cosocle b -> (cocone_composable (colimit_to_cocone b a) b & cocone_compose (colimit_to_cocone b a) b = a).
proof: Proof. ir. uh H0; ee. uh H2; ee. util (H3 a). am. am. cp (choose_pr H4). cbv beta in H5. ee. am. uh H2; ee. util (H3 a). am. am. cp (choose_pr H4). cbv beta in H5. ee. am. Qed.
imports: Arith limits