proposition: Lemma oppc_cocone_compose : forall c u, cocone_composable u c -> oppc (cocone_compose u c) = (cone_compose (oppc c) (flip u)).
proof: Proof. ir. assert (cone_composable (oppc c) (flip u)). ap cone_composable_oppc. rw flip_flip. am. ap cone_extensionality. app is_cone_oppc. app is_cocone_cocone_compose. rww is_cone_cone_compose. rw vertex_oppc. rw vertex_cocone_compose. rw vertex_cone_compose. rw source_flip. tv. uh H; ee. ap (mor_arrow_like H1). rw socle_oppc. rw cosocle_cocone_compose. rw socle_cone_compose. rw socle_oppc. tv. uh H; ee; am. app is_cocone_cocone_compose. ir. rwi cone_source_oppc H1. rwi cocone_source_cocone_compose H1. cp H1. rwi ob_opp H1. wri cone_source_oppc H2. rw edge_oppc. sy. rw edge_cone_compose. rw coedge_cocone_compose. rw edge_oppc. rw cone_target_oppc. rw comp_opp. rw flip_flip. rw flip_flip. tv. rw mor_opp. rw flip_flip. ap mor_coedge. am. uh H; ee; am. rw mor_opp. rw flip_flip. uh H; ee; am. rw source_flip. rw target_flip. rw target_coedge. uh H; ee; sy; am. am. uh H; ee; am. uh H; ee; alike. apply mor_arrow_like with (cocone_target c). ap mor_coedge. am. uh H; ee; am. uh H; ee; am. am. uh H; ee; am. am. am. am. rww cocone_source_cocone_compose. app is_cocone_cocone_compose. uh H; ee; am. app is_cocone_cocone_compose. Qed.
imports: Arith limits