proposition: Lemma is_limit_cone_compose : forall a u, is_limit a -> cone_composable a u -> invertible (cone_target a) u -> is_limit (cone_compose a u).
proof: Proof. ir. assert (lem1: is_cone (cone_compose a u)). rww is_cone_cone_compose. uhg; ee. uhg; ee. am. ir. assert (mor (cone_target a) u0). uh H2; ee. rwi cone_target_cone_compose H5. am. assert (mor (cone_target a) v). uh H3; ee. rwi cone_target_cone_compose H6; am. assert (source u = target u0). sy. uh H2; ee. rwi vertex_cone_compose H8; am. assert (source u = target v). sy. uh H3; ee. rwi vertex_cone_compose H9; am. assert (mor (cone_target a) u). uh H0; ee. am. rwi cone_compose_cone_compose H4. rwi cone_compose_cone_compose H4. uh H; ee. uh H; ee. assert (comp (cone_target a) u u0 = comp (cone_target a) u v). ap H11. uhg; ee. am. rww mor_comp. rww target_comp. lu. uhg; ee. am. rww mor_comp. rw target_comp. lu. lu. lu. lu. am. transitivity (comp (cone_target a) (inverse (cone_target a) u) (comp (cone_target a) u u0)). wr assoc. rw left_inverse. rw left_id. tv. rww ob_source. am. sy; am. tv. am. ap mor_inverse. am. am. am. rw source_inverse. tv. am. am. tv. rw H12. wr assoc. rw left_inverse. rw left_id. tv. rww ob_source. am. sy; am. tv. am. app mor_inverse. am. am. rww source_inverse. am. tv. am. app show_composable. am. app show_composable. assert (lema: target u = vertex a). lu. uhg; ee. am. ir. assert (lem0 : socle b = socle a). rwi socle_cone_compose H3. am. assert (lem2: composable (cone_target a) (inverse (cone_target a) u) (cone_to_limit b a)). ap show_composable. app mor_inverse. app mor_cone_to_limit. rw source_inverse. rww target_cone_to_limit. lu. sh (comp (cone_target a) (inverse (cone_target a) u) (cone_to_limit b a)). ee. uhg; ee. am. rw cone_target_cone_compose. rww mor_comp. app mor_inverse. app mor_cone_to_limit. rww source_inverse. rww target_cone_to_limit. rww target_comp. rww target_inverse. assert (cone_target a = cone_target (cone_compose a u)). rww cone_target_cone_compose. rww vertex_cone_compose. app mor_inverse. app mor_cone_to_limit. rww source_inverse. rww target_cone_to_limit. assert (mor (cone_target a) u). uh H0; ee; am. rw cone_compose_cone_compose. wr assoc. rww right_inverse. rw left_id. rw cone_compose_cone_to_limit. tv. am. am. am. rww ob_target. app mor_cone_to_limit. rw target_cone_to_limit. sy; am. am. am. am. tv. am. app mor_inverse. app mor_cone_to_limit. rww target_inverse. rww source_inverse. rww target_cone_to_limit. tv. am. ap show_composable. am. rww mor_comp. app mor_inverse. app mor_cone_to_limit. rww source_inverse. rww target_cone_to_limit. rww target_comp. rww target_inverse. app mor_inverse. app mor_cone_to_limit. rww source_inverse. rww target_cone_to_limit. Qed.
imports: Arith nat_trans