proposition: Lemma oppc_cone_compose : forall c u, cone_composable c u -> oppc (cone_compose c u) = (cocone_compose (flip u) (oppc c)).
proof: Proof. ir. assert (cocone_composable (flip u) (oppc c)). ap cocone_composable_oppc. rw flip_flip. am. ap cocone_extensionality. app is_cocone_oppc. rww is_cone_cone_compose. app is_cocone_cocone_compose. rw vertex_oppc. rw vertex_cone_compose. rw vertex_cocone_compose. rw target_flip. tv. uh H; ee. ap (mor_arrow_like H1). rw cosocle_oppc. rw socle_cone_compose. rw cosocle_cocone_compose. rw cosocle_oppc. tv. uh H; ee; am. rww is_cone_cone_compose. ir. assert (is_cone c). uh H; ee; am. rwi cocone_source_oppc H1. rwi cone_source_cone_compose H1. cp H1. rwi ob_opp H1. rw coedge_oppc. sy. rw coedge_cocone_compose. rw edge_cone_compose. rw coedge_oppc. rw cocone_target_oppc. rw comp_opp. rw flip_flip. rw flip_flip. tv. wr cocone_target_oppc. rw cocone_target_oppc. rw mor_opp. rw flip_flip. uh H; ee; am. uh H; ee; am. uh H; ee; am. rw mor_opp. rw flip_flip. ap mor_edge. am. uh H; ee; am. rw source_flip. rw target_flip. rw source_edge. uh H; ee; am. am. am. apply mor_arrow_like with (cone_target c). app mor_edge. uh H; ee; alike. am. am. am. am. am. rw cocone_source_oppc. am. am. rww cone_source_cone_compose. rww is_cone_cone_compose. rww is_cone_cone_compose. Qed.
imports: Arith limits