proposition: Lemma cone_to_limit_cone_compose : forall a b u, is_limit b -> cone_composable a u -> socle a = socle b -> cone_to_limit (cone_compose a u) b = comp (cone_target b) (cone_to_limit a b) u.
proof: Proof. ir. set (k:= comp (cone_target b) (cone_to_limit a b) u). assert (cone_target a = cone_target b). uf cone_target. rww H1. assert (lem1 : is_cone a). lu. transitivity (cone_to_limit (cone_compose b k) b). uf k. wr cone_compose_cone_compose. rw cone_compose_cone_to_limit. tv. lu. am. am. rww cone_composable_cone_to_limit. app show_composable. app mor_cone_to_limit. wr H2. lu. rww source_cone_to_limit. sy; lu. rww cone_to_limit_cone_compose1. uf k. uhg; ee. uh H; ee. uh H; ee; am. rww mor_comp. app mor_cone_to_limit. wr H2. lu. rww source_cone_to_limit. sy; lu. rw target_comp. rww target_cone_to_limit. app mor_cone_to_limit. wr H2; lu. rww source_cone_to_limit. sy; lu. Qed.
imports: Arith nat_trans