proposition: Lemma cocone_composable_oppc : forall c u, cone_composable c (flip u) -> cocone_composable u (oppc c).
proof: Proof. ir. uhg; ee. ap is_cocone_oppc. uh H; ee; am. rw cocone_target_oppc. rw mor_opp. uh H; ee; am. uh H; ee. am. rw vertex_oppc. uh H; ee. wr H1. rww target_flip. apply by_cases with (Arrow.like u). ir. am. ir. rwi flip_not_like H0. apply mor_arrow_like with (cone_target c); am. am. Qed.
imports: Arith limits