proposition: Lemma cone_to_limit_cone_compose1 : forall a u, is_limit a -> cone_composable a u -> cone_to_limit (cone_compose a u) a = u.
proof: Proof. ir. assert (lem1 : is_limit a). am. uh H; ee. uh H; ee. ap H2. uhg; ee. am. ap mor_cone_to_limit. rww is_cone_cone_compose. am. rw socle_cone_compose. tv. tv. rw target_cone_to_limit. tv. rww is_cone_cone_compose. am. rw socle_cone_compose. tv. am. rw cone_compose_cone_to_limit. tv. rww is_cone_cone_compose. am. rww socle_cone_compose. Qed.
imports: Arith nat_trans