proposition: Lemma comp_cone_to_limit_inversely : forall a b c, is_limit a -> is_limit b -> socle a = socle b -> cone_target a = c -> comp c (cone_to_limit a b) (cone_to_limit b a) = id c (vertex b).
proof: Proof. ir. assert (cone_target b = c). uf cone_target. wr H1. am. cp H; cp H0. uh H4; uh H5; ee. uh H4; uh H5. ee. assert (composable c (cone_to_limit a b) (cone_to_limit b a)). ap show_composable. app mor_cone_to_limit. sy; am. app mor_cone_to_limit. sy; am. sy; am. rww source_cone_to_limit. rww target_cone_to_limit. sy; am. ap H8. uhg; ee. am. rw H3. rww mor_comp. ap mor_cone_to_limit. am. am. am. sy; am. app mor_cone_to_limit. sy; am. sy; am. rw source_cone_to_limit. rww target_cone_to_limit. sy; am. am. am. am. rw target_comp. rww target_cone_to_limit. app mor_cone_to_limit. sy; am. app mor_cone_to_limit. sy; am. sy; am. rw source_cone_to_limit. rww target_cone_to_limit. sy; am. am. am. am. uhg; ee. am. rw H3. ap mor_id. wr H3. ap ob_vertex. am. rw target_id. tv. wr H3; app ob_vertex. wr H3. wr cone_compose_cone_compose. rw cone_compose_cone_to_limit. rw cone_compose_cone_to_limit. rw cone_compose_id. tv. am. am. am. sy; am. am. am. am. uhg; ee. am. app mor_cone_to_limit. rww target_cone_to_limit. rww H3. Qed.
imports: Arith nat_trans