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