proposition: Lemma cocone_composable_rw : forall c u, is_cocone c -> mor (cocone_target c) u -> source u = vertex c -> cocone_composable u c = True.
proof: Proof. ir. uf cocone_composable. app iff_eq; ir; try tv. xd. Qed.
imports: Arith limits